| Age | Commit message (Expand) | Author |
|---|
| 2004-01-13 | Suppression de Rsyntax en v8 | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2003-12-24 | changement de pose en set (pose n'etait pas utilise avec la semantique | barras |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-05 | power associe a droite | marche |
| 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 | Utilisation du total_order non constructif | herbelin |
| 2003-11-28 | Protection contre les renommages; redondances | herbelin |
| 2003-11-19 | Restauration compatibilite 7.4 pour le Hint Unfold Rgt | herbelin |
| 2003-11-15 | Meilleure solution pour la compatibilite | herbelin |
| 2003-11-12 | MAJ INZ | herbelin |
| 2003-11-02 | Restauration preference Rge a Rle pour compatibilite... | herbelin |
| 2003-11-02 | Restauration preference Rge a Rle pour compatibilite...; petit nettoyage | herbelin |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-20 | R passe dans Set ! | herbelin |
| 2003-10-17 | 20 est uniquement associatif a gauche | herbelin |
| 2003-10-16 | lettac -> set | barras |
| 2003-10-16 | Pour eviter des regles redondantes en v7 | herbelin |
| 2003-10-16 | FTC_P2 maintenant dans RIneq | herbelin |
| 2003-10-16 | Ajout de quelques lemmes cles | herbelin |
| 2003-10-15 | Affichage = au lieu de == en v7 | herbelin |
| 2003-10-13 | Notations pour l'exponentiation | herbelin |
| 2003-10-10 | Notation '^' | herbelin |
| 2003-10-03 | Cacher les .v8 | herbelin |
| 2003-09-23 | Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type... | herbelin |
| 2003-09-21 | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin |
| 2003-09-19 | Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr... | herbelin |
| 2003-09-19 | Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem... | herbelin |
| 2003-09-12 | Ajout et MAJ commandes de scopes | herbelin |
| 2003-09-12 | Bind et Delimit pour R | herbelin |
| 2003-09-12 | Bind et Delimit pour R | herbelin |
| 2003-06-12 | INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu... | herbelin |
| 2003-05-29 | niveau 49 devient next | herbelin |
| 2003-05-24 | "INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals | herbelin |
| 2003-05-21 | Bug | herbelin |
| 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-04-29 | En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ... | herbelin |
| 2003-04-17 | Divers | herbelin |
| 2003-04-17 | <> maintenant standard | 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 | Local 'o' | herbelin |
