aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.ml
Commit message (Expand)AuthorAge
* Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
* Statment -> StatementGravatar Hugo Herbelin2018-06-03
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Mini-restructurationGravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* Mise en place de motifs récursifs dans Notation; quelques simplifications au...Gravatar herbelin2004-03-17
* Implantation de l'option 'format' des NotationsGravatar herbelin2003-10-01
* Les notations hors scope s'empilent maintenant comme des scopes neGravatar herbelin2003-09-30
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* *** empty log message ***Gravatar barras2003-03-12
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
* Calcul de l'associativité même pour les Grammar avec plusieurs clausesGravatar herbelin2002-12-03
* Re-déplacement du résultat de Grammar au niveau constr_exprGravatar herbelin2002-12-02
* Affinement de la gestion des niveaux toujours; type ETBigintGravatar herbelin2002-11-28
* Affinement encoreGravatar herbelin2002-11-28
* Affinement de la gestion des niveauxGravatar herbelin2002-11-28
* Correction sur commit précédentGravatar herbelin2002-11-27
* OubliGravatar herbelin2002-11-26
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* MAJ delimiters et niveaux d'associativiteGravatar herbelin2002-11-25
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...Gravatar herbelin2002-10-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29