aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.ml4
Commit message (Expand)AuthorAge
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* Hugly temporary notationGravatar sacerdot2004-09-29
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* syntax compatibility fixGravatar corbinea2004-07-02
* instantiate entry: constr -> lconstrGravatar corbinea2004-06-30
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 17:29:41 +0000