| Age | Commit message (Expand) | Author |
|---|
| 2003-05-14 | Amelioration presentation | herbelin |
| 2003-05-14 | Amelioration affichage | herbelin |
| 2003-05-14 | Suppression de 'R' dans la notation == entre | herbelin |
| 2003-05-14 | Suppression de 'R' dans la notation == entre | herbelin |
| 2003-05-14 | Deplacement lemmes sur fact de Reals vers Arith | herbelin |
| 2003-05-13 | Nouveaux lemmes | herbelin |
| 2003-05-13 | Nouveaux lemmes (sur proposition de Nijmegen) | herbelin |
| 2003-05-13 | Nouveaux lemmes (sur proposition de Nijmegen) | herbelin |
| 2003-05-09 | ajout inverse relation bien fondee | mohring |
| 2003-05-07 | coqide: toolbar/autosave | monate |
| 2003-04-29 | Blancs | herbelin |
| 2003-04-29 | Notations | herbelin |
| 2003-04-29 | Implicit Types | herbelin |
| 2003-04-29 | Ajout ChoiceFacts | herbelin |
| 2003-04-29 | Blancs | herbelin |
| 2003-04-29 | En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ... | 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 | Divers | herbelin |
| 2003-04-17 | <> maintenant standard | herbelin |
| 2003-04-17 | Intégration DatatypesSyntax à Datatypes | herbelin |
| 2003-04-17 | Syntaxe 'x=y:>T' | herbelin |
| 2003-04-16 | suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom different | letouzey |
| 2003-04-16 | sumboolT, sumorT, sigTT, SigT redondants | herbelin |
| 2003-04-14 | Cosmetique | herbelin |
| 2003-04-14 | Local 'o' | herbelin |
| 2003-04-12 | Open Scope en Local | herbelin |
| 2003-04-10 | Open Scope remplace Import | herbelin |
| 2003-04-10 | Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter | herbelin |
| 2003-04-10 | Remplacement Import par Open Scope en v8 | herbelin |
| 2003-04-09 | cast de nil | herbelin |
| 2003-04-09 | nil en implicite dans la v8 | herbelin |
| 2003-04-09 | Ajout Open Scope | 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-04-09 | Renommage K; equivalence JMeq et eq_dep sur Type | herbelin |
| 2003-04-09 | Defined | herbelin |
| 2003-04-09 | Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import". | herbelin |
| 2003-04-09 | Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import" | herbelin |
| 2003-04-07 | Nommage explicite des hypotheses introduites quand le nom existe aussi comme ... | herbelin |
| 2003-04-07 | Cosmetique | herbelin |
| 2003-04-07 | Espaces superflus | herbelin |
| 2003-04-03 | Documentation, généralisation à eq sur Type, preuves d'équivalence des | herbelin |
| 2003-03-31 | Ajout double_plus | herbelin |
| 2003-03-31 | Ajout Implicit Variable Type | 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-29 | Implicit Variables Type | herbelin |
