aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.mli
AgeCommit message (Expand)Author
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