| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2003-03-28 | Pas d'associativité gauche au niveau 3 en vieille syntaxe ! | 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-02-27 | Restructuration des hints pour qu'Auto fasse moins de détours et les | herbelin |
| 2003-02-14 | Ajout du theoreme de Cesaro | desmettr |
| 2003-02-13 | Modifications dans une tactique toplevel | delahaye |
| 2003-01-30 | Pb de parenthèse dans "Check (S (plus O O))" | herbelin |
