coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-01	- Addition to the Reals theory :	thery
	- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-28	[stdlib]Reals: use “lia” rather than “omega”	Vincent Laporte

2019-09-16	Remove library-specific code for `Import`.	Maxime Dénès
	Libraries are now handled like other modules.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-07-17	Remove fourier plugin	Maxime Dénès
	As stated in the manual, the fourier tactic is subsumed by lra.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-03-22	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond
	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).
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-09-17	Add some missing Proof statements.	Guillaume Melquiond

2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
	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.
2014-04-16	Fixing missing headers.	Hugo Herbelin

2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-11	finish the rearrangement for removing the sin_PI2 axiom. This new version	bertot
	- 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
2012-06-11	Adds the proof of PI_ineq, plus some other smarter ways to approximate PI	bertot
	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