aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/g_rewrite.ml4
Commit message (Expand)AuthorAge
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* Removing unused tactics in rewrite.Gravatar Pierre-Marie Pédrot2014-01-14
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* 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