aboutsummaryrefslogtreecommitdiff
path: root/parsing/extend.ml
AgeCommit message (Expand)Author
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2005-12-30Mini-restructurationherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications au...herbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-03-12*** empty log message ***barras
2002-12-15Meilleure factorisation des entrées NEXT internesherbelin
2002-12-03Calcul de l'associativité même pour les Grammar avec plusieurs clausesherbelin
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_exprherbelin
2002-11-28Affinement de la gestion des niveaux toujours; type ETBigintherbelin
2002-11-28Affinement encoreherbelin
2002-11-28Affinement de la gestion des niveauxherbelin
2002-11-27Correction sur commit précédentherbelin
2002-11-26Oubliherbelin
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
2002-11-25MAJ delimiters et niveaux d'associativiteherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin