aboutsummaryrefslogtreecommitdiff
path: root/parsing/q_util.ml4
AgeCommit message (Expand)Author
2006-11-02gestion speciale du niveau 5 des ltacbarras
2006-10-24Hack peu élégant pour permettre de parser des listes avec séparateurs dans herbelin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-06-23Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT E...herbelin
2006-06-23Suppresion redondance interp_entry_name entre Q_util et Argextendherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Branchement sur Util.loc et abstraction vis a vis de dummy_locherbelin
2003-11-13factorisation et generalisation des clausesbarras
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin