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