From 00150efde21b9e493a1578dc35a30025fc79d9d7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 12:23:04 +0000
Subject: La bonne modif des Unfold

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

diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index aa4fbef8be..d3f0464eea 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -44,7 +44,7 @@ Save.
 
 (**********)
 Lemma fp_R0:(frac_part R0)==R0.
-Unfold frac_part; Unfold Int_part;Elim (archimed R0);
+Unfold frac_part; Unfold Int_part; Elim (archimed R0);
  Intros; Unfold Rminus;
  Elim (Rplus_ne (Ropp (IZR `(up R0)-1`))); Intros a b;
  Rewrite b;Clear a b;Rewrite <- Z_R_minus;Cut (up R0)=`1`.
-- 
cgit v1.2.3