| Age | Commit message (Expand) | Author |
|---|
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-16 | Syntax error | herbelin |
| 2003-10-16 | Suppression des surcharge de regles de grammaire en v7 | herbelin |
| 2003-10-03 | Cacher les .v8 | herbelin |
| 2003-09-26 | 'Open Local Scope' en attendant que le core_scope sache se mettre devant impl... | herbelin |
| 2003-09-26 | Passage de Destruct a NewDestruct; '-' pour negb | herbelin |
| 2003-09-23 | Remplacement de Induction/Destruct par NewInduction/NewDestruct | herbelin |
| 2003-06-13 | FSets, mais pas compile' par make world | filliatr |
| 2003-06-10 | Import nat_scope | herbelin |
| 2003-05-29 | Ne pas mettre d'associatif a droite au niveau 3 en V7 | herbelin |
| 2003-05-21 | Notations | herbelin |
| 2003-04-29 | Notations | herbelin |
| 2003-04-09 | Defined | herbelin |
| 2003-01-06 | bit vectors | filliatr |
| 2002-07-09 | Making the sumbool functions transparent, so that they can used to | bertot |
| 2002-06-20 | ZArith_base, Zbool, Bool_nat | filliatr |
| 2002-05-06 | Standardisation | herbelin |
| 2002-04-17 | Uniformisation (Qed/Save et Implicits Arguments) | herbelin |
| 2002-03-04 | Nouveau Rewrite-in plus economique | barras |
| 2002-02-28 | Ajout andb_true_eq pour PolyList.list_beq | herbelin |
| 2002-02-14 | option -dump-glob pour coqdoc | filliatr |
| 2001-09-27 | Simplification de deux preuves. En outre ca simplifie leur extraction. | letouzey |
| 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-20 | Library doc adjustments (until page 140) | coq |
| 2001-04-19 | BoolEq.v, une egalite generique a valeur dans bool | mohring |
| 2001-04-19 | Mise de (*i autour CVS info | mohring |
| 2001-04-11 | documentation automatique de la bibliothèque standard | filliatr |
| 2001-03-30 | Ajout de lemmes sur les booleens | mohring |
| 2001-03-15 | entetes | filliatr |
| 2001-02-01 | - coqc : option -image | filliatr |
| 2000-11-28 | Elimination du ' | delahaye |
| 2000-11-05 | Plus besoin de débrancher la preuve qui ne passait pas | herbelin |
| 2000-05-22 | Séparation des tokens -> et ~ | herbelin |
| 2000-05-03 | Ajout du langage de tactiques | delahaye |
| 2000-05-02 | portage Omega (mais toujours pas Zpower et Zlogarithm) | filliatr |
| 2000-03-16 | mise sous CVS | filliatr |
