| Age | Commit message (Expand) | Author |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-29 | remove many excessive open Util & Errors in mli's | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-03-26 | Slight change in the semantics of arguments scopes: scopes can no | herbelin |
| 2012-03-20 | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Simplified the way internalization_data (i.e. bindings of bound vars | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-03-29 | Several bug-fixes and improvements of coqdoc | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-14 | - Addition of "Reserved Infix" continued. | herbelin |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-08-11 | Add support for "Infix ... := constr" instead of just "Infix ... := ref". | herbelin |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2007-02-24 | Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ) | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-23 | Simplifification de vernac_expr li l'abandon du traducteur | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-22 | Traitement plus clair, notamment pour Locate, de quand quoter les composantes... | herbelin |
| 2003-10-14 | Changement 'as notation' en 'where notation' | herbelin |
| 2003-10-01 | Implantation de l'option 'format' des Notations | herbelin |
| 2003-09-30 | Ajout 'Close Scope'. | herbelin |
| 2003-09-19 | parsing | herbelin |
| 2003-09-12 | Ajout 'Print Scopes' et 'Bind Scope with classes' | herbelin |
| 2003-09-10 | Traduction de Distfix | herbelin |
| 2003-05-22 | Ajout V8Notation | herbelin |
| 2003-04-29 | Prise en compte des syntaxes v8 dans Uninterpreted Notation | herbelin |
| 2003-04-17 | Ajout "at next level" dans Notation | herbelin |
| 2003-04-11 | Ajout option 'Local' à Infix et Notation | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2002-11-29 | Raffinement syntaxe Infix | herbelin |
| 2002-11-25 | MAJ delimiters et niveaux d'associativite | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-22 | Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;... | herbelin |
| 2002-10-13 | Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha... | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2001-03-15 | entetes | filliatr |
| 2001-03-09 | protection contre certaines exceptions levees par marshal_{in,out} | barras |
| 2001-03-01 | Déplacement de qualid dans Nametab, hors du noyau | herbelin |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-11-22 | Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's... | herbelin |