aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/RIneq.v
AgeCommit message (Expand)Author
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-06changed statements of Rpower_lt and Rle_power and addedYves Bertot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-07Add some hints to the "real" database to automatically discharge literal comp...Guillaume Melquiond
2017-04-02Simplify some proofs.Guillaume Melquiond
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-03-22Make IZR use a compact representation of integers.Guillaume Melquiond
2017-03-22Simplify some proofs using ring and field.Guillaume Melquiond
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-03-10Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Guillaume Melquiond
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2013-12-03Remove a useless hypothesis from Rle_Rinv.Guillaume Melquiond
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-05Modifications and rearrangements to remove the action that sin (PI/2) = 1bertot
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Added the following lemmas to homogenize Reals a bit:gmelquio
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
2009-02-06Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]herbelin
2008-04-06Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :herbelin
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-04- Amélioration de la présentation de RIneq, même si un nettoyage desherbelin
2008-03-23Une passe sur les réels:herbelin
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-10-27simplif de la partie ML de ring/fieldbarras
2006-10-17Mise en forme des theoriesnotin
2006-09-28separation de RealFieldbarras
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2005-03-29Missing translating a 'O' into a '0' (again)herbelin
2004-07-16Nouvelle en-têteherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:07:54 +0000