aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Expand)AuthorAge
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* *** empty log message ***Gravatar barras2003-03-12
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Subst (tout court)Gravatar filliatr2002-09-16
* tactique Subst x1 ... xnGravatar filliatr2002-09-11
* tactique SubstGravatar filliatr2002-07-17
* Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...Gravatar herbelin2002-06-05
* Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...Gravatar herbelin2002-06-05
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29