From e37c1b1114a37224d36531cee438561b04d798d0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 13 Jul 2005 22:29:44 +0000
Subject: Détection d'un Fold incorrect suite à correction bug #986

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

diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index d20b896a53..3e121ecf68 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -489,8 +489,7 @@ elim s; intro.
 left; apply a.
 right; apply b.
 cut (Un_growing (fun n:nat => sum_f_R0 An n)).
-intro; set (l1 := sum_f_R0 An N).
-fold l1 in r.
+intro; set (l1 := sum_f_R0 An N) in r.
 unfold Un_cv in H; cut (0 < l1 - l).
 intro; elim (H _ H2); intros.
 set (N0 := max x N); cut (N0 >= x)%nat.
-- 
cgit v1.2.3