aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/RIneq.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-06-22Elementary properties about IZR for generic use.Hugo Herbelin
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
2020-04-01- Addition to the Reals theory :thery
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-10-28[stdlib]Reals: use “lia” rather than “omega”Vincent Laporte
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-08-09Switch constructive Rlt to sort Type, to make it compute laterVincent Semeria
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-07-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:32 +0000