aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.mli
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 08:31:54 +0000