| Age | Commit message (Expand) | Author |
|---|
| 2004-03-12 | ajout decimal_exp pour interpreter les notations decimales | mohring |
| 2004-03-03 | ide: silent behavior better, save icon, -byte works | marche |
| 2004-02-28 | MAJ Commentaires | herbelin |
| 2004-02-12 | Ajout delimiteur pour bool_scope | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2004-02-10 | backtrack implicit dans Bvector | marche |
| 2004-02-09 | patch Bvector: args implicites | marche |
| 2004-01-27 | MAJ simplification | herbelin |
| 2004-01-13 | Suppression de Rsyntax en v8 | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-09 | Commentaires en v8 | herbelin |
| 2003-12-24 | Ajout delimiteur et arguments de scope pour list | herbelin |
| 2003-12-24 | changement de pose en set (pose n'etait pas utilise avec la semantique | barras |
| 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-12-04 | Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p... | herbelin |
| 2003-12-01 | Ratage standardisation Rge_monotony en Rmult_ge_compat_r | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-29 | Notation locale pour Rpower | herbelin |
| 2003-11-29 | Ajout lemmes, simplification preuve de SeqProp | herbelin |
| 2003-11-29 | ground->firstorder, cc-> congruence, CC final commit | corbinea |
| 2003-11-29 | Utilisation du total_order non constructif | herbelin |
| 2003-11-29 | Report de lemmes de Znumtheory dans Zabs ou BinInt | herbelin |
| 2003-11-28 | Protection contre les renommages; redondances | herbelin |
| 2003-11-24 | Renoncement de la compatibilite des noms qualifies au profit de la compatibil... | herbelin |
| 2003-11-22 | Compatibilite | herbelin |
| 2003-11-21 | Simplification; ajout Zcompare_antisym | herbelin |
| 2003-11-21 | ajout Pnat (suite) | herbelin |
| 2003-11-21 | ajout Pnat (suite) | herbelin |
| 2003-11-21 | Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e... | herbelin |
| 2003-11-21 | Tri et typo | herbelin |
| 2003-11-19 | ajout de Znumtheory.v dans ZArith | letouzey |
| 2003-11-19 | Restauration compatibilite 7.4 pour le Hint Unfold Rgt | herbelin |
| 2003-11-18 | Un nouveau lemme redondant ... | herbelin |
| 2003-11-18 | Deplacement ZERO_le_inj dans Zorder | herbelin |
| 2003-11-15 | Meilleure solution pour la compatibilite | herbelin |
| 2003-11-14 | Pour les .v8 | herbelin |
| 2003-11-14 | Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base | herbelin |
| 2003-11-14 | cosmetique | herbelin |
| 2003-11-14 | Presentation | herbelin |
| 2003-11-14 | Ordre standard pour l'associativite | herbelin |
| 2003-11-14 | Quelques oublis pour que les notations marchent bien | herbelin |
| 2003-11-14 | Bug implicit arguments | herbelin |
| 2003-11-14 | Automatisation de la traduction de iff_trans; renommage IF | herbelin |
| 2003-11-14 | Backtrack sur Peano | herbelin |
| 2003-11-14 | Nouveaux lemmes 'canoniques'; compatibilite | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
