Library doc adjustments (until page 140)

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

5 files changed, 8 insertions, 12 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).
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 9e79ee3a0..31d4c9430 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -170,12 +170,12 @@ Apply multiset_twist2.
 Qed.
 
 
-(* theory of minter to do similarly 
+(*i theory of minter to do similarly 
 Require Min.
 (* multiset intersection *)
 Definition minter := [m1,m2:multiset]
     (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
-*)
+i*)
 
 End multiset_defs.
 
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 699c5f362..3e1837078 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -274,4 +274,3 @@ Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
 	singlx incl_add : sets v62.
 
 
-(* $Id$ *)
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index c7e8e7d05..90c055775 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -61,6 +61,3 @@ Hints Resolve definition_of_noetherian : sets v62.
 Hints Unfold  Noetherian : sets v62.
 
 
-
-
-(* $Id$ *)
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 12f267873..ced2a75f9 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Sets  as characteristic functions *)
 
@@ -199,12 +199,12 @@ Apply uniset_twist2.
 Qed.
 
 
-(* theory of minter to do similarly 
+(*i theory of minter to do similarly 
 Require Min.
 (* uniset intersection *)
 Definition minter := [m1,m2:uniset]
     (Charac [a:A](andb (charac m1 a)(charac m2 a))).
-*)
+i*)
 
 End defs.