aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.mli
Commit message (Expand)AuthorAge
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Add occurence extra argGravatar msozeau2008-01-30
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Bug in replace tactics introduced in r9073 (overlap between replace .. with a...Gravatar jforest2006-08-23
* Forgot a file in previous commit Gravatar jforest2006-08-22
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Hugly temporary notationGravatar sacerdot2004-09-29
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* Code obsoleteGravatar herbelin2003-11-08
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29