aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
Commit message (Expand)AuthorAge
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Utilisation du section_path pour le parsing des notations primitives,Gravatar herbelin2006-02-04
* Adaptation message d'erreur au cas des stringGravatar herbelin2006-01-31
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...Gravatar herbelin2006-01-08
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02