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, 2 insertions, 5 deletions

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 248c8ce73..5a9ea513c 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1114,7 +1114,7 @@ apply Ropp_gt_lt_contravar;
      Rmin (delta / 2) ((b + - c) / 2))) in |- *; apply Rplus_lt_le_0_compat;
  [ assumption
  | rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption ].
-ring.
+unfold Rminus; ring.
 rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
 replace
  ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
@@ -1306,10 +1306,7 @@ prove_sup0.
 replace (2 * (c + (a - c) / 2)) with (a + c).
 rewrite double.
 apply Rplus_lt_compat_l; assumption.
-ring.
-rewrite <- Rplus_assoc.
-rewrite <- double_var.
-ring.
+field; discrR.
 assumption.
 unfold Rabs in |- *; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))).
 intro; generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro;