| Age | Commit message (Expand) | Author |
| 2003-10-14 | Changement 'as notation' en 'where notation' | herbelin |
| 2003-10-14 | Argument de except, error implicite seulement en v8; Changement 'as notation'... | herbelin |
| 2003-10-14 | Argument de None implicite seulement en v8 | herbelin |
| 2003-10-13 | Argument implicite pour None, error, except | herbelin |
| 2003-10-13 | Enregistrement '^' en v8 | herbelin |
| 2003-10-11 | mise a jour nouvelle syntaxe | barras |
| 2003-10-10 | nat_scope ouvert par defaut | herbelin |
| 2003-10-10 | identity est equivalent sur Type (sauf sans argument) | herbelin |
| 2003-10-10 | type_scope | herbelin |
| 2003-10-10 | Suppression de definitions equivalentes | herbelin |
| 2003-10-10 | Delimiters N devient 'nat' | herbelin |
| 2003-10-10 | changement nouvelle syntaxe (pt fixes) | barras |
| 2003-10-03 | Cacher les .v8 | herbelin |
| 2003-09-28 | well_founded_induction de nouveau transparent | letouzey |
| 2003-09-23 | Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type... | herbelin |
| 2003-09-22 | traducteur: affiche les commentaires a l'interieur des commandes | barras |
| 2003-09-21 | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin |
| 2003-09-21 | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin |
| 2003-09-21 | Nettoyage | herbelin |
| 2003-09-19 | Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem... | herbelin |
| 2003-09-12 | Suppression DatatypesSyntax et PeanoSyntax qui était vides | herbelin |
| 2003-09-12 | Bind et Delimit pour nat | herbelin |
| 2003-09-11 | Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ... | herbelin |
| 2003-08-10 | Affichage {}+{}, niveau paire au plus haut | herbelin |
| 2003-07-08 | recursion bien fondee sur des pairs | filliatr |
| 2003-06-10 | Suppression d'une occurrence superflue d'argument de type dans Notation sacha... | herbelin |
| 2003-06-10 | Deplacement delimiteur T dans Notations | herbelin |
| 2003-05-29 | Bug niveau | herbelin |
| 2003-05-29 | Ne pas mettre d'associatif a droite au niveau 3 en V7 | herbelin |
| 2003-05-27 | 'only parsing' pour le passage de trucT a truc | herbelin |
| 2003-05-22 | V8Notation | herbelin |
| 2003-05-22 | Ajout V8Notation | herbelin |
| 2003-05-21 | Concentration des notations officielles dans Init/Notations; restructuration ... | herbelin |
| 2003-04-29 | Blancs | herbelin |
| 2003-04-28 | Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot | letouzey |
| 2003-04-17 | Intégration DatatypesSyntax à Datatypes | herbelin |
| 2003-04-17 | Intégration DatatypesSyntax à Datatypes | herbelin |
| 2003-04-17 | Syntaxe 'x=y:>T' | herbelin |
| 2003-04-09 | Activation des implicites pour la v8 | herbelin |
| 2003-04-09 | Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import" | herbelin |
| 2003-03-31 | Suppression des alias eqT/exT/exT2 en nouvelle syntaxe | herbelin |
| 2003-03-31 | Notation eqT superflue | herbelin |
| 2003-03-29 | eq fusionne avec eqT et devient par défaut sur Type, | herbelin |
| 2003-03-29 | Déplacement de minus dans Peano | herbelin |
| 2003-03-28 | notations <>, Assumption avec existentiel, replace term | mohring |
| 2003-03-21 | *** empty log message *** | barras |
| 2003-03-14 | *** empty log message *** | barras |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-01-30 | Pb de parenthèse dans "Check (S (plus O O))" | herbelin |
| 2002-12-15 | Une entrée spéciale "annot" pour les piquants | herbelin |