aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* entetesGravatar filliatr2001-03-15
* protection contre certaines exceptions levees par marshal_{in,out}Gravatar barras2001-03-09
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...Gravatar herbelin2001-01-31
* Réorganisation autour de globalize_constrGravatar herbelin2000-11-24
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Prise en compte noms longsGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageGravatar herbelin2000-10-24
* Import de Infix au RequireGravatar herbelin2000-10-23
* Correction bug affichage des infixGravatar herbelin2000-10-16
* Restructuration printer et parserGravatar herbelin2000-01-07
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* premier debugageGravatar filliatr1999-12-05
* module MetasyntaxGravatar filliatr1999-12-01