| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Remove some dead-code (thanks to ocaml warnings) |  Pierre Letouzey | 2014-03-05 |
| * | 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-11-02 |
| * | Removing uses of Evar.add in class-related functions. |  ppedrot | 2013-10-06 |
| * | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
| * | Splitting Class_tactics between code and CAMLP4/5 declarations. | ppedrot | 2013-10-04 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |