| Age | Commit message (Expand) | Author |
|---|
| 2004-08-01 | Commentaires coqdoc | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-04-06 | sumbool et sumor affich avec 'if' si possible | herbelin |
| 2004-03-29 | Commentaires | herbelin |
| 2004-03-17 | Definition de la notation de la paire par un motif recursif | herbelin |
| 2004-02-28 | MAJ Commentaires | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2004-01-09 | Commentaires en v8 | herbelin |
| 2003-12-23 | Finalement, espacement autour du ':' pour a la fois exists, forall et fun | herbelin |
| 2003-12-21 | Affichage sur le modèle du forall pour le exists | herbelin |
| 2003-12-16 | Duplication temporaire des règles de syntaxe des paires | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-05 | power associe a droite | marche |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-21 | Tri et typo | herbelin |
| 2003-11-14 | Automatisation de la traduction de iff_trans; renommage IF | herbelin |
| 2003-11-14 | Backtrack sur Peano | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-12 | Ajout lemme projections | herbelin |
| 2003-11-12 | %type au lieu de %T | herbelin |
| 2003-11-12 | Lemmes dans un sens plus naturel | herbelin |
| 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 |
