aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Machin.v
Commit message (Expand)AuthorAge
* 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
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* 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