From 99f4c55d9b9eb1130bff54a1ff9028b442141231 Mon Sep 17 00:00:00 2001
From: bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 15 Dec 2006 15:30:59 +0000
Subject: Changement dans ring et field, beaucoup de correction d'erreurs,
 maintenant les differentes tactics marchent mieux mais le code est moche ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Cos_plus.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Reals/Cos_plus.v')

diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 82b0a3949..1ef4f1ec4 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -486,7 +486,7 @@ Proof.
   apply le_trans with (pred N).
   assumption.
   apply le_pred_n.
-  ring_nat.
+  ring.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
   apply le_trans with (2 * S (S (n0 + n)))%nat.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   omega.
   right.
   unfold Rdiv in |- *; rewrite Rmult_comm.
-- 
cgit v1.2.3