aboutsummaryrefslogtreecommitdiff
path: root/parsing/pptactic.mli
AgeCommit message (Expand)Author
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-23Correction printer des Tactic Notationherbelin
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-12*** empty log message ***barras
2003-02-13Debugger plus informatifdelahaye
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin