| Commit message (Expand) | Author | Age |
* | ajout decimal_exp pour interpreter les notations decimales | mohring | 2004-03-12 |
* | ide: silent behavior better, save icon, -byte works | marche | 2004-03-03 |
* | MAJ Commentaires | herbelin | 2004-02-28 |
* | Ajout delimiteur pour bool_scope | herbelin | 2004-02-12 |
* | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin | 2004-02-12 |
* | backtrack implicit dans Bvector | marche | 2004-02-10 |
* | patch Bvector: args implicites | marche | 2004-02-09 |
* | MAJ simplification | herbelin | 2004-01-27 |
* | Suppression de Rsyntax en v8 | herbelin | 2004-01-13 |
* | bugs avec Pose et Assert | barras | 2004-01-09 |
* | Commentaires en v8 | herbelin | 2004-01-09 |
* | 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-24 |
* | Finalement, espacement autour du ':' pour a la fois exists, forall et fun | herbelin | 2003-12-23 |
* | Affichage sur le modèle du forall pour le exists | herbelin | 2003-12-21 |
* | Duplication temporaire des règles de syntaxe des paires | herbelin | 2003-12-16 |
* | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras | 2003-12-15 |
* | power associe a droite | marche | 2003-12-05 |
* | Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p... | herbelin | 2003-12-04 |
* | Ratage standardisation Rge_monotony en Rmult_ge_compat_r | herbelin | 2003-12-01 |
* | 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-29 |
* | Protection contre les renommages; redondances | herbelin | 2003-11-28 |
* | Renoncement de la compatibilite des noms qualifies au profit de la compatibil... | herbelin | 2003-11-24 |
* | Compatibilite | herbelin | 2003-11-22 |
* | 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-21 |
* | ajout de Znumtheory.v dans ZArith | letouzey | 2003-11-19 |
* | Restauration compatibilite 7.4 pour le Hint Unfold Rgt | herbelin | 2003-11-19 |
* | Un nouveau lemme redondant ... | herbelin | 2003-11-18 |
* | Deplacement ZERO_le_inj dans Zorder | herbelin | 2003-11-18 |
* | Meilleure solution pour la compatibilite | herbelin | 2003-11-15 |
* | 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-14 |
* | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras | 2003-11-13 |