remove Fourier Failure warnings.

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

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 7c3834914..35f254e13 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.