option -dump-glob pour coqdoc

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

4 files changed, 25 insertions, 24 deletions

diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 40389087e..af202239e 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -42,11 +42,12 @@ Inductive Empty_set : Ensemble :=
 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. \\
-   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)]. *)
+(** NB: The following definition builds-in equality of elements in [U] as 
+   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)]. *)
 
 Inductive Singleton [x:U] : Ensemble :=
       In_singleton: (In (Singleton x) x).
@@ -92,9 +93,8 @@ Definition Strict_Included : Ensemble -> Ensemble -> Prop :=
 Definition Same_set : Ensemble -> Ensemble -> Prop :=
    [B, C: Ensemble] (Included B C) /\ (Included C B).
 
-(*************************************)
-(*******  Extensionality Axiom *******)
-(*************************************)
+(** Extensionality Axiom *)
+
 Axiom Extensionality_Ensembles:
    (A,B: Ensemble) (Same_set A B) -> A == B.
 Hints Resolve Extensionality_Ensembles.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 31d4c9430..4abaaaa60 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -34,7 +34,7 @@ Definition SingletonBag := [a:A]
 Definition multiplicity : multiset -> A -> nat :=
   [m:multiset][a:A]let (f) = m in (f a).
 
-(* multiset equality *)
+(** multiset equality *)
 Definition meq := [m1,m2:multiset]
     (a:A)(multiplicity m1 a)=(multiplicity m2 a).
 
@@ -60,7 +60,7 @@ Induction x; Induction y; Auto.
 Qed.
 Hints Immediate meq_sym.
 
-(* multiset union *)
+(** multiset union *)
 Definition munion := [m1,m2:multiset]
     (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))).
 
@@ -112,8 +112,8 @@ Qed.
 Hints Resolve meq_right.
 
 
-(* Here we should make multiset an abstract datatype, by hiding Bag,
-   munion, multiplicity; all further properties are proved abstractly *)
+(** Here we should make multiset an abstract datatype, by hiding [Bag],
+    [munion], [multiplicity]; all further properties are proved abstractly *)
 
 Lemma munion_rotate :
    (x,y,z:multiset)(meq (munion x (munion y z)) (munion z (munion x y))).
@@ -151,7 +151,7 @@ Apply meq_sym; Apply munion_ass.
 Apply meq_left; Apply munion_perm_left.
 Qed.
 
-(* specific for treesort *)
+(** specific for treesort *)
 
 Lemma treesort_twist1 : (x,y,z,t,u:multiset) (meq u (munion y z)) ->
    (meq (munion x (munion u t)) (munion (munion y (munion x t)) z)).
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 686ea973e..03a8b7428 100755
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -10,8 +10,8 @@
 
 (* G. Huet 1-9-95 *)
 
-(* We consider a Set U, given with a commutative-associative operator op,
-and a congruence cong; we show permutation lemmas *)
+(** We consider a Set [U], given with a commutative-associative operator [op],
+    and a congruence [cong]; we show permutation lemmas *)
 
 Section Axiomatisation.
 
@@ -29,7 +29,7 @@ Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)).
 Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z).
 Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x).
 
-(* Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
+(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
 
 Lemma cong_congr :
  (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)).
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index ced2a75f9..d4e5c44b9 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -8,10 +8,11 @@
 
 (*i $Id$ i*)
 
-(* Sets  as characteristic functions *)
+(** Sets as characteristic functions *)
 
 (* G. Huet 1-9-95 *)
 (* Updated Papageno 12/98 *)
+
 Require Bool.
 
 Implicit Arguments On.
@@ -41,12 +42,12 @@ Definition In : uniset -> A -> Prop :=
      [s:uniset][a:A](charac s a)=true.
 Hints Unfold In.
 
-(* uniset inclusion *)
+(** uniset inclusion *)
 Definition incl := [s1,s2:uniset]
     (a:A)(leb (charac s1 a) (charac s2 a)).
 Hints Unfold incl.
 
-(* uniset equality *)
+(** uniset equality *)
 Definition seq := [s1,s2:uniset]
     (a:A)(charac s1 a) = (charac s2 a).
 Hints Unfold seq.
@@ -86,7 +87,7 @@ Unfold seq.
 Induction x; Induction y; Simpl; Auto.
 Qed.
 
-(* uniset union *)
+(** uniset union *)
 Definition union := [m1,m2:uniset]
     (Charac [a:A](orb (charac m1 a)(charac m2 a))).
 
@@ -137,10 +138,10 @@ Qed.
 Hints Resolve seq_right.
 
 
-(* All the proofs that follow duplicate [Multiset_of_A] *)
+(** All the proofs that follow duplicate [Multiset_of_A] *)
 
-(* Here we should make uniset an abstract datatype, by hiding Charac,
-   union, charac; all further properties are proved abstractly *)
+(** Here we should make uniset an abstract datatype, by hiding [Charac],
+    [union], [charac]; all further properties are proved abstractly *)
 
 Require Permut.
 
@@ -180,7 +181,7 @@ Apply seq_sym; Apply union_ass.
 Apply seq_left; Apply union_perm_left.
 Qed.
 
-(* specific for treesort *)
+(** specific for treesort *)
 
 Lemma treesort_twist1 : (x,y,z,t,u:uniset) (seq u (union y z)) ->
    (seq (union x (union u t)) (union (union y (union x t)) z)).