aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/RIneq.v
Commit message (Expand)AuthorAge
* Add some hints to the "real" database to automatically discharge literal comp...Gravatar Guillaume Melquiond2017-04-07
* Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
* Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
* Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
* Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
* Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
* Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]Gravatar herbelin2009-02-06
* Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :Gravatar herbelin2008-04-06
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* - Amélioration de la présentation de RIneq, même si un nettoyage desGravatar herbelin2008-04-04
* Une passe sur les réels:Gravatar herbelin2008-03-23
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 10:30:24 +0000