aboutsummaryrefslogtreecommitdiff
path: root/tactics/extraargs.ml4
AgeCommit message (Expand)Author
2004-09-29Hugly temporary notationsacerdot
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
2004-07-16Nouvelle en-tĂȘteherbelin
2004-07-02syntax compatibility fixcorbinea
2004-06-30instantiate entry: constr -> lconstrcorbinea
2004-06-29moved instantiate binding to extratacticscorbinea
2003-11-08Code obsoleteherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin