From f3bd9b51d74319a0ad0f0bb4694d03dc00b4dcef Mon Sep 17 00:00:00 2001
From: roconnor
Date: Thu, 24 Jan 2008 14:38:12 +0000
Subject: remove Fourier Failure warnings.

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

diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 7c38349143..35f254e133 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -62,12 +62,12 @@ set (f:=fun n => (if HP n then (1/2)^n else 0)%R).
  clear X.
  exists N.
  intros n m Hn Hm.
- replace e with (e/2 + e/2)%R by fourier.
+ replace e with (e/2 + e/2)%R by field.
  set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *.
  assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2).
   apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R.
    apply R_dist_tri.
-  replace (/(1 - 1/2)) with 2 in HN by fourier.
+  replace (/(1 - 1/2)) with 2 in HN by field.
   cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R.
    intros Z.
    apply Rplus_lt_compat.
-- 
cgit v1.2.3