aboutsummaryrefslogtreecommitdiff
path: root/parsing/extend.ml
AgeCommit message (Expand)Author
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-28[gramlib] Refactor gramlib interface.Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-08-19[pcoq] Remove unneeded casting operators.Emilio Jesus Gallego Arias
2019-08-19[parsing] Move pcoq-specific parts in extend to pcoq.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
2018-06-03Statment -> StatementHugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2012-05-29Extend become a mli-only file in intf/letouzey
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:39:37 +0000