From a3837fa9dd60b7b8528e2e31c98682528c694dcd Mon Sep 17 00:00:00 2001
From: coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 23 Apr 2001 15:07:44 +0000
Subject: Minor layout adjustments for Library doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1672 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/DiscrR.v      | 2 +-
 theories/Reals/Rbase.v       | 3 ++-
 theories/Reals/SplitAbsolu.v | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'theories/Reals')

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index a5155163b..8fe437561 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i        $Id$       i*)
 
 Require Rbase.
 
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index f8b88f9c6..b6024dcc7 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1314,7 +1314,8 @@ Save.
 
 (**********)
 Lemma single_z_r_R1
-  : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``->z=x.
+  : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``
+    ->z=x.
 Intros; Apply one_IZR_r_R1 with r; Auto.
 Save.
 
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index 3b423aefb..ba2fbf535 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*      $Id$      *)
 
 Require Export Rbasic_fun.
 
-- 
cgit v1.2.3