aboutsummaryrefslogtreecommitdiff
path: root/tactics/extratactics.ml4
AgeCommit message (Expand)Author
2004-03-18Backtrack sur commit 1.20herbelin
2004-03-17Desactivation de la syntaxe v7 de Hint Rewrite en v8herbelin
2004-03-10Ajout tactiques stepl et stepr de Nimègueherbelin
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...herbelin
2004-03-01Ajout 'replace in'herbelin
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-12petits changements de syntaxebarras
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-19Extension de l'utilisation de contradictionherbelin
2003-10-10Cablage en dur de inversionherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-12*** empty log message ***barras
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-09-16Subst (tout court)filliatr
2002-09-11tactique Subst x1 ... xnfilliatr
2002-07-17tactique Substfilliatr
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...herbelin
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...herbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin