| Age | Commit message (Expand) | Author |
|---|
| 2003-04-07 | Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite | herbelin |
| 2003-04-07 | Options d'affichage maintenant dans Constrextern | herbelin |
| 2003-04-07 | Options d'affichage maintenant dans Constrextern | herbelin |
| 2003-04-04 | maj | filliatr |
| 2003-04-03 | Documentation, généralisation à eq sur Type, preuves d'équivalence des | herbelin |
| 2003-04-03 | Backtrack du commit de Christine, qui posait probleme avec FTC | letouzey |
| 2003-04-03 | Légères simplifications code de Field; message d'erreur si pas égalité | herbelin |
| 2003-04-03 | maj | filliatr |
| 2003-04-02 | espace manquant | herbelin |
| 2003-04-01 | remplace == par = dans la tactique field pour que le debugger marche a nouvea... | narboux |
| 2003-04-01 | maj | filliatr |
| 2003-04-01 | Déplacement with_option dans Options | herbelin |
| 2003-04-01 | Correction bug #261 + amélioration nommage | herbelin |
| 2003-04-01 | Extension de Replace aux égalités entre preuves | herbelin |
| 2003-04-01 | Fail 1 pour traverser le match | herbelin |
| 2003-04-01 | maj | filliatr |
| 2003-03-31 | MAJ | herbelin |
| 2003-03-31 | Noms absolus | herbelin |
| 2003-03-31 | Ajout double_plus | herbelin |
| 2003-03-31 | Ajout Implicit Variable Type | herbelin |
| 2003-03-31 | Plus de eqT; message Fail | herbelin |
| 2003-03-31 | Ajout d'un message à FailTac | herbelin |
| 2003-03-31 | Ajout d'un message à FailTac; localisation des appels à des tactiques défi... | herbelin |
| 2003-03-31 | Mise en place d'un traducteur de noms v7->v8 | herbelin |
| 2003-03-31 | Ajout d'un choix 'onlyparse' | herbelin |
| 2003-03-31 | Suppression des alias eqT/exT/exT2 en nouvelle syntaxe | herbelin |
| 2003-03-31 | Ajout VernacReserve et suppression des types re-inferables | herbelin |
| 2003-03-31 | Restauration de make_all_different (disparu depuis version 1.74) car sinon de... | herbelin |
| 2003-03-31 | Bug pattern_occ_hyp_list | herbelin |
| 2003-03-31 | Correcting a bug occuring when the mimicked function had a | courtieu |
| 2003-03-31 | Notation eqT superflue | herbelin |
| 2003-03-31 | factorisation des "constant" dans les contrib/* ( maintenant dans coqlib ) | corbinea |
| 2003-03-31 | minus a changé d'emplacement -> omega pas content | letouzey |
| 2003-03-31 | maj | filliatr |
| 2003-03-29 | eq fusionne avec eqT et devient par défaut sur Type, | herbelin |
| 2003-03-29 | indentation | herbelin |
| 2003-03-29 | Déplacement de minus dans Peano | herbelin |
| 2003-03-29 | Implicit Variables Type | herbelin |
| 2003-03-29 | Implicit Variables Type dans les inductive | herbelin |
| 2003-03-29 | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin |
| 2003-03-29 | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin |
| 2003-03-29 | maj | filliatr |
| 2003-03-28 | coqide: command window maj. | monate |
| 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-28 | coqide: bug undo corrige | monate |
| 2003-03-28 | Réparation bug de l'unification. En effet, avant l'instanciation d'une evar | clrenard |
| 2003-03-28 | Fixed Relative names not,iff in Camlp4 quotation. | corbinea |
| 2003-03-27 | coqide: bugfix du C-C pendant Undo+paren_highlight | monate |
| 2003-03-27 | MAJ des mots-clés, Definition, Theorem, ... | herbelin |
