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