diff options
| author | herbelin | 2004-03-01 17:47:15 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-01 17:47:15 +0000 |
| commit | e6e53fa4d491c38c3785399aeaeae59dc22f09c4 (patch) | |
| tree | 682f8563d05e5eda93497557eb0223afbcfabf3f | |
| parent | 2a4ab4bb5720de115edb7bfbb2124194c1334cc6 (diff) | |
code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5410 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/fourier/Fourier_util.v | 9 |
1 files 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. |