mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

1 files changed, 4 insertions, 7 deletions

diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index dc365842b..0dfe58552 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -88,11 +88,9 @@ rewrite Rplus_0_r;
  replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
   with (Un (S (S (2 * S N)))); [ idtac | ring ].
 apply H.
-apply INR_eq; rewrite mult_INR; repeat rewrite S_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 apply HrecN.
-apply INR_eq; repeat rewrite S_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 Qed.
 
 (* A more general inequality *)
@@ -293,8 +291,7 @@ rewrite (Rmult_comm (INR (2 * S n + 1))); rewrite Rmult_assoc;
 do 2 rewrite Rmult_1_r; apply le_INR.
 replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
 apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite plus_INR;
- do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+ring_nat.
 apply not_O_INR; discriminate.
 apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
  [ discriminate | ring ].
@@ -445,4 +442,4 @@ rewrite Rmult_1_l; replace (2 + 1) with 3; [ prove_sup0 | ring ].
 rewrite Rplus_comm; pattern 1 at 1 in |- *; rewrite <- Rplus_0_r;
  apply Rplus_lt_compat_l; prove_sup0.
 assumption.
-Qed.
\ No newline at end of file
+Qed.