aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.mli
AgeCommit message (Expand)Author
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-30Fix a small notation/scope bug:vsiles
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-10-05Essai de changement de sémantique du %scope : herbelin
2006-02-04Utilisation du section_path pour le parsing des notations primitives,herbelin
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...herbelin
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...herbelin
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin