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/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 479d381d4..9d1ba7381 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -182,13 +182,13 @@ Section sequence.
 
     assert (Hs0: forall n, sum n = 0).
     intros n.
-    specialize (Hm1 (sum n) (ex_intro _ _ (refl_equal _))).
+    specialize (Hm1 (sum n) (ex_intro _ _ (eq_refl _))).
     apply Rle_antisym with (2 := proj1 (Hsum n)).
     now rewrite <- Hm.
 
     assert (Hub: forall n, Un n <= l - eps).
     intros n.
-    generalize (refl_equal (sum (S n))).
+    generalize (eq_refl (sum (S n))).
     simpl sum at 1.
     rewrite 2!Hs0, Rplus_0_l.
     unfold test.
@@ -238,7 +238,7 @@ Section sequence.
     rewrite (IHN H6), Rplus_0_l.
     unfold test.
     destruct Rle_lt_dec.
-    apply refl_equal.
+    apply eq_refl.
     now elim Rlt_not_le with (1 := r).
 
     destruct (le_or_lt N n) as [Hn|Hn].
@@ -272,13 +272,13 @@ Section sequence.
   Proof.
     intro; induction  N as [| N HrecN].
     split with (Un 0); intros; rewrite (le_n_O_eq n H);
-      apply (Req_le (Un n) (Un n) (refl_equal (Un n))).
+      apply (Req_le (Un n) (Un n) (eq_refl (Un n))).
     elim HrecN; clear HrecN; intros; split with (Rmax (Un (S N)) x); intros;
       elim (Rmax_Rle (Un (S N)) x (Un n)); intros; clear H1;
         inversion H0.
     rewrite <- H1; rewrite <- H1 in H2;
       apply
-        (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (refl_equal (Un n))))).
+        (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (eq_refl (Un n))))).
     apply (H2 (or_intror (Un n <= Un (S N)) (H n H3))).
   Qed.