aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.mli
Commit message (Expand)AuthorAge
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)Gravatar herbelin2007-02-24
* 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
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* Traitement plus clair, notamment pour Locate, de quand quoter les composantes...Gravatar herbelin2003-11-22
* Changement 'as notation' en 'where notation'Gravatar herbelin2003-10-14
* Implantation de l'option 'format' des NotationsGravatar herbelin2003-10-01
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
* parsingGravatar herbelin2003-09-19
* Ajout 'Print Scopes' et 'Bind Scope with classes'Gravatar herbelin2003-09-12
* Traduction de DistfixGravatar herbelin2003-09-10
* Ajout V8NotationGravatar herbelin2003-05-22
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* *** empty log message ***Gravatar barras2003-03-12
* Raffinement syntaxe InfixGravatar herbelin2002-11-29
* MAJ delimiters et niveaux d'associativiteGravatar herbelin2002-11-25
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...Gravatar herbelin2002-10-22
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...Gravatar herbelin2002-10-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* 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
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* 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
* module MetasyntaxGravatar filliatr1999-12-01