coq/theories/Reals/vo.itarget, branch master The formal proof system drop vo.itarget files and compute the corresponding the corresponding values automatically instead 2017-06-01T15:33:19+00:00 Matej Kosik 2017-03-23T11:56:24+00:00 718d61a54157733bca61ed84c0ba3761cd52720f 






Legacy Ring and Legacy Field migrated to contribs
2012-07-05T22:51:11+00:00

letouzey

2012-07-05T22:51:11+00:00

2ed6aeb03fc0e25a47223189d8444cbb6b749f2d

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7





 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7







finish the rearrangement for removing the sin_PI2 axiom.  This new version
2012-06-11T15:32:59+00:00

bertot

2012-06-11T15:32:59+00:00

4dab5938805ec41237b1bdce5efa308e37932cd0

- 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





- 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
2012-06-11T09:00:00+00:00

bertot

2012-06-11T09:00:00+00:00

a5c2bbab10ba5f26ad289e1b911db69294946c55

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





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







Factorisation between Makefile and ocamlbuild systems : .vo to compile are in */*/vo.itarget
2009-12-09T16:45:42+00:00

letouzey

2009-12-09T16:45:42+00:00

cfc9e109a653047b7ca73224525bba67a8c3a571

 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7





 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7