From e6e53fa4d491c38c3785399aeaeae59dc22f09c4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Mar 2004 17:47:15 +0000
Subject: code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5410 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/fourier/Fourier_util.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/contrib/fourier/Fourier_util.v b/contrib/fourier/Fourier_util.v
index dcc45b66e4..e52597878c 100644
--- a/contrib/fourier/Fourier_util.v
+++ b/contrib/fourier/Fourier_util.v
@@ -136,14 +136,9 @@ replace 0 with (- -0).
 replace (- (n * / d)) with (- n * / d).
 replace (-0) with 0.
 red in |- *.
-try exact H0.
 apply Ropp_gt_lt_contravar.
-replace (- (n * / d)) with (- n * / d).
-replace (-0) with 0.
 red in |- *.
-try exact H0.
-ring.
-ring.
+exact H0.
 ring.
 ring.
 ring.
@@ -224,4 +219,4 @@ Qed.
  
 Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y.
 exact Rnot_lt_ge.
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3