aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Ranalysis5.v
Commit message (Expand)AuthorAge
* Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\
| * Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-03-04
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Add some hints to the "real" database to automatically discharge literal comp...Gravatar Guillaume Melquiond2017-04-07
* Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* 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
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11