| Age | Commit message (Expand) | Author |
|---|
| 2003-11-12 | petits changements de syntaxe | barras |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
| 2003-10-28 | Ordre (symbolique) des Require | herbelin |
| 2003-10-28 | Passage de la notations de paire dans core_scope | herbelin |
| 2003-10-28 | Passage des notations de type dans type_scope | herbelin |
| 2003-10-28 | Ajout %core; MAJ niveau connecteurs logique | herbelin |
| 2003-10-23 | Commentaires | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-21 | Maintenant avant Datatypes | herbelin |
| 2003-10-21 | ajouts | herbelin |
| 2003-10-17 | Des implicites plus 'naturels' pour eq_ind, identity_ind and co | herbelin |
| 2003-10-16 | nouvelle syntaxe de ltac | barras |
| 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 |
