| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-09-14 | Rewrite.apply_strategy uses the same return type as strategies. | Pierre-Marie Pédrot |
| 2014-09-14 | Proper type for rewrite strategy results. | Pierre-Marie Pédrot |
| 2014-09-11 | Use an AST for strategy names. | Matthieu Sozeau |
| 2014-07-14 | Redo PMP's patch to rewriting to make it purely functional using state passing. | Matthieu Sozeau |
| 2014-06-11 | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-01-14 | Removing unused tactics in rewrite. | Pierre-Marie Pédrot |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-09-26 | Opacifying the type of strategies. | ppedrot |
| 2013-09-26 | Splitting Rewrite into a code part and a CAMLP4-dependent one. | ppedrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |