aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.ml4
Commit message (Expand)AuthorAge
* 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