coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-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 version	bertot	2012-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 PI	bertot	2012-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