Library doc adjustments (until page 140)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 7 insertions, 7 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 966a755c5..e7829b00e 100755
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -85,14 +85,14 @@ Proof     (* We draw the diagram ! *)
 Theorem caseRxy : (coherence y z).
 Proof (Rstar_Rstar' x z h2 
       ([v:A][w:A](coherence y w))
-      (coherence_sym x y (Rstar_coherence x y h1))  (* case x=z *)
-      Diagram).                                     (* case x->v->*z *)
+      (coherence_sym x y (Rstar_coherence x y h1))  (*i case x=z i*)
+      Diagram).                                     (*i case x->v->*z i*)
 End Newman_.
 
 Theorem Ind_proof : (coherence y z).
 Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z))
-        (Rstar_coherence x z h2)                    (* case x=y*)
-        caseRxy).                                   (* case x->u->*z *)
+        (Rstar_coherence x z h2)                    (*i case x=y i*)
+        caseRxy).                                   (*i case x->u->*z i*)
 End Induct.
 
 Theorem Newman : (x:A)(confluence x).
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5ee00157..a5c81e2e3 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (****************************************************************************)
-(*                      Bruno Barras Cristina Cornes                        *)
+(*                      Bruno Barras, Cristina Cornes                       *)
 (*                                                                          *)
 (*  Some of these definitons were taken from :                              *)
 (*     Constructing Recursion Operators in Type Theory                      *)
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index 0df3af6b4..a0aaed9ad 100755
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -10,8 +10,8 @@
 
 (* Properties of a binary relation R on type A *)
 
-  Parameter A : Type.  
-  Parameter R : A->A->Prop.  
+Parameter A : Type.  
+Parameter R : A->A->Prop.  
 
 (* Definition of the reflexive-transitive closure R* of R *)
 (* Smallest reflexive P containing R o P *)