aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Le caractère ² fait planter make docGravatar notin2006-10-27
* Mise en forme des theoriesGravatar notin2006-10-17
* separation de RealFieldGravatar barras2006-09-28
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Renommage sqtr_lem_1 (bug 1189)Gravatar notin2006-07-17
* Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...Gravatar herbelin2006-07-11
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...Gravatar herbelin2006-05-22
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...Gravatar herbelin2006-05-22
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* New unification can solve the problem without eta-expansion, Gravatar msozeau2006-04-10
* Nommage explicite de certains "intro" pour préserver la compatibilitéGravatar herbelin2006-03-28
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
* Missing translating a 'O' into a '0' (again)Gravatar herbelin2005-03-29
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* ajout decimal_exp pour interpreter les notations decimalesGravatar mohring2004-03-12
* Suppression de Rsyntax en v8Gravatar herbelin2004-01-13
* bugs avec Pose et AssertGravatar barras2004-01-09
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* power associe a droiteGravatar marche2003-12-05
* Ratage standardisation Rge_monotony en Rmult_ge_compat_rGravatar herbelin2003-12-01
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Notation locale pour RpowerGravatar herbelin2003-11-29
* Ajout lemmes, simplification preuve de SeqPropGravatar herbelin2003-11-29
* Utilisation du total_order non constructifGravatar herbelin2003-11-29
* Protection contre les renommages; redondancesGravatar herbelin2003-11-28
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
* Meilleure solution pour la compatibiliteGravatar herbelin2003-11-15
* MAJ INZGravatar herbelin2003-11-12
* Restauration preference Rge a Rle pour compatibilite...Gravatar herbelin2003-11-02
* Restauration preference Rge a Rle pour compatibilite...; petit nettoyageGravatar herbelin2003-11-02
* Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...Gravatar herbelin2003-10-30
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* R passe dans Set !Gravatar herbelin2003-10-20
* 20 est uniquement associatif a gaucheGravatar herbelin2003-10-17
* lettac -> setGravatar barras2003-10-16
* Pour eviter des regles redondantes en v7Gravatar herbelin2003-10-16
* FTC_P2 maintenant dans RIneqGravatar herbelin2003-10-16
* Ajout de quelques lemmes clesGravatar herbelin2003-10-16
* Affichage = au lieu de == en v7Gravatar herbelin2003-10-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:06:51 +0000