| Age | Commit message (Expand) | Author |
| 2009-11-16 | Some lemmas about dependent choice + extensions of Compare_dec + | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2008-05-12 | MAJ et bricoles diverses | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2007-06-22 | Ajout exist & cie à la table des hints par symétrie avec ex_intro & | herbelin |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-03-17 | Modification des propriétés (svn:executable) | notin |
| 2005-05-19 | Documentation | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-04-06 | sumbool et sumor affich avec 'if' si possible | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-10-28 | Passage des notations de type dans type_scope | herbelin |
| 2003-10-23 | Commentaires | herbelin |
| 2003-10-14 | Argument de except, error implicite seulement en v8; Changement 'as notation'... | herbelin |
| 2003-10-13 | Argument implicite pour None, error, except | herbelin |
| 2003-09-23 | Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type... | herbelin |
| 2003-05-21 | Concentration des notations officielles dans Init/Notations; restructuration ... | herbelin |
| 2003-04-09 | Activation des implicites pour la v8 | herbelin |
| 2002-11-26 | Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques | herbelin |
| 2002-11-25 | Retablissement SynDef Value/Error | herbelin |
| 2002-11-24 | Généralisation de l'utilisation de Notation | herbelin |
| 2002-02-14 | option -dump-glob pour coqdoc | filliatr |
| 2002-01-31 | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring |
| 2002-01-09 | MAJ des Id pour coqweb | herbelin |
| 2001-11-14 | Suppression d'Export redondants | herbelin |
| 2001-09-27 | and_rec redondant | letouzey |
| 2001-08-30 | Fin de la modif Exc/option | mohring |
| 2001-08-29 | ajout option , Exc --> option, et lemmes dans les theories | mohring |
| 2001-08-05 | Expérimentation de NewDestruct et parfois NewInduction | herbelin |
| 2001-04-11 | documentation automatique de la bibliothèque standard | filliatr |
| 2001-03-30 | Introduction d'une preuve de False_rec | mohring |
| 2001-03-15 | entetes | filliatr |
| 1999-12-13 | fichiers prelude Coq | filliatr |