aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.ml4
Commit message (Expand)AuthorAge
...
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* Code obsoleteGravatar herbelin2003-11-08
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* 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