| Age | Commit message (Expand) | Author |
|---|---|---|
| 2013-11-02 | More Proofview.Goal.enter. | aspiwack |
| 2013-11-02 | A whole new implemenation of the refine tactic. | aspiwack |
| 2013-11-02 | A newly introduced variable inside a named context is no longer α-renamed. | aspiwack |
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-06 | Removing uses of Evar.add in class-related functions. | ppedrot |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-10-04 | Splitting Class_tactics between code and CAMLP4/5 declarations. | ppedrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |