aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/RIneq.v
Commit message (Expand)AuthorAge
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* simplif de la partie ML de ring/fieldGravatar barras2006-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
* Missing translating a 'O' into a '0' (again)Gravatar herbelin2005-03-29
* Nouvelle en-têteGravatar herbelin2004-07-16
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* 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
* Ajout lemmes, simplification preuve de SeqPropGravatar 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...; petit nettoyageGravatar herbelin2003-11-02
* lettac -> setGravatar barras2003-10-16
* Ajout de quelques lemmes clesGravatar herbelin2003-10-16
* INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...Gravatar herbelin2003-06-12
* "INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans RealsGravatar herbelin2003-05-24
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* Open Scope en LocalGravatar herbelin2003-04-12
* Remplacement Import par Open Scope en v8Gravatar herbelin2003-04-10
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
* Ajout Implicit Variable TypeGravatar herbelin2003-03-31
* *** empty log message ***Gravatar barras2003-03-21
* *** empty log message ***Gravatar barras2003-03-12
* Restructuration des hints pour qu'Auto fasse moins de détours et lesGravatar herbelin2003-02-27
* Suppression de INR2 / Conséquence logique de la nouvelle représentation des...Gravatar desmettr2003-01-21
* Renommage de Rbase.v en RIneq.vGravatar desmettr2003-01-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:51:17 +0000