Library doc adjustments (until page 140)

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 0ddad8578..40389087e 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -43,10 +43,10 @@ Inductive Full_set : Ensemble :=
      Full_intro: (x: U) (In Full_set x).
 
 (* NB The following definition builds-in equality of elements in U as 
-   Leibniz equality.
+   Leibniz equality. \\
    This may have to be changed if we replace U by a Setoid on U with its own
-   equality eqs, with 
-      [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
+   equality eqs, with  
+     [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
 Inductive Singleton [x:U] : Ensemble :=
       In_singleton: (In (Singleton x) x).