Backport to 8.4 the recent changes concerning PI by Y. Bertot

Original commit messages:

* Modifications and rearrangements to remove the axiom that sin (PI/2) = 1
  Beware that the definition of PI changes in the process

* Adds the proof of PI_ineq, plus some other smarter ways to approximate PI
  and of course, the definition of atan (the inverse of tan, from R to
  (-PI/2, PI/2)

* finish the rearrangement for removing the sin_PI2 axiom.  This new version
  - 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.

* These files are displaced from Rtrigo.v and Ranalysis_reg.v

* make sure that documentation compilation works after adding files for
  arc tangent and computations of PI approximations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15549 85f007b7-540e-0410-9357-904b9bb8a0f7
BinInt: a forgotten scope for a notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15550 85f007b7-540e-0410-9357-904b9bb8a0f7
Notation: a new annotation "compat 8.x" extending "only parsing"

 Suppose we declare : Notation foo := bar (compat "8.3").
 Then each time foo is used in a script :

 - By default nothing particular happens (for the moment)

 - But we could get a warning explaining that
   "foo is bar since coq > 8.3".
   For that, either use the command-line option -verb-compat-notations
   or the interactive command "Set Verbose Compat Notations".

 - There is also a strict mode, where foo is forbidden : the previous
   warning is now an error.
   For that, either use the command-line option -no-compat-notations
   or the interactive command "Unset Compat Notations".

 When Coq is launched in compatibility mode (via -compat 8.x),
 using a notation tagged "8.x" will never trigger a warning or error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15551 85f007b7-540e-0410-9357-904b9bb8a0f7
ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15552 85f007b7-540e-0410-9357-904b9bb8a0f7
Open Scope can now also accepts delimiters (e.g. Z).
Of course, scope names (e.g. Z_scope) are still accepted.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15553 85f007b7-540e-0410-9357-904b9bb8a0f7
Open Local Scope ---> Local Open Scope, same with Notation and alii

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15554 85f007b7-540e-0410-9357-904b9bb8a0f7
Kills the useless tactic annotations "in |- *"

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15555 85f007b7-540e-0410-9357-904b9bb8a0f7
MSetRBT : elementary arith proofs instead of calls to lia

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15556 85f007b7-540e-0410-9357-904b9bb8a0f7
Some cleanup in recent proofs concerning pi

 Initial idea was to just avoid compat notations such
 as Z_of_nat --> Z.of_nat, but I ended trying to improve
 a few proofs...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15557 85f007b7-540e-0410-9357-904b9bb8a0f7
More cleanup in Ring_polynom and EnvRing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15558 85f007b7-540e-0410-9357-904b9bb8a0f7
Restore the compatibility notation Compare.not_eq_sym

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15559 85f007b7-540e-0410-9357-904b9bb8a0f7
BinPos/BinInt/BinNat : fix some argument scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15560 85f007b7-540e-0410-9357-904b9bb8a0f7
Ring_polynom : a restricted simpl instead of a unfold;fold

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15561 85f007b7-540e-0410-9357-904b9bb8a0f7
verbose compat notations : nicer option name

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15562 85f007b7-540e-0410-9357-904b9bb8a0f7