aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
AgeCommit message (Expand)Author
2007-05-10Prise en compte réversibilité des notations de la forme "Notation Nil := @n...herbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-01-10Suite commit restructuration discharge (application du type deherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-10-23Add a flush for a warning.courtieu
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
2006-10-05Essai de changement de sémantique du %scope : herbelin
2006-09-23Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-02-04Utilisation du section_path pour le parsing des notations primitives,herbelin
2006-01-31Adaptation message d'erreur au cas des stringherbelin
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
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-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-01-03HUGE COMMITsacerdot
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin