aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Machin.v
Commit message (Collapse)AuthorAge
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
| | | | As stated in the manual, the fourier tactic is subsumed by lra.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
* 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
| | | | | | | | | | | | | corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
|
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
| | | | | | | | | | | | | | | - provides the atan function - shows that this function is equal between -1 and 1 to a function defined with power series - establishes the equality with the PI value as given by the alternated series constructed with PI_tg - provides a smarter theorem to compute approximations of PI, based on a formula in the same family as the one used by John Machin in 1706 Dependencies between files have been rearranged so that the new theorems are loaded with the library Reals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11
and of course, the definition of atan (the inverse of tan, from R to (-PI/2, PI/2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 03:07:14 +0000