option -dump-glob pour coqdoc

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

6 files changed, 48 insertions, 48 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c9052de6c..528e61ab0 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
+(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
 Require Le.
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index ae62962ea..15e9fe670 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -8,13 +8,13 @@
 
 (*i $Id$ i*)
 
-(* A Library for finite sets, implemented as lists *)
-(* A Library with similar interface will soon be available under
-  the name TreeSet in the theories/Trees directory *)
+(** A Library for finite sets, implemented as lists 
+    A Library with similar interface will soon be available under
+    the name TreeSet in the theories/Trees directory *)
 
-(* PolyList is loaded, but not exported *)
-(* This allow to "hide" the definitions, functions and theorems of PolyList
-   and to see only the ones of ListSet *)
+(** PolyList is loaded, but not exported.
+    This allow to "hide" the definitions, functions and theorems of PolyList
+    and to see only the ones of ListSet *)
 
 Require PolyList.
 
@@ -48,7 +48,7 @@ Section first_definitions.
                    end
     end.
  
-  (* If a belongs to x, removes a from x. If not, does nothing *)
+  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
   Fixpoint set_remove [a:A; x:set] : set :=
     Cases x of
     | nil => empty_set
@@ -72,7 +72,7 @@ Section first_definitions.
     | (cons a1 y1) => (set_add a1 (set_union x y1))
     end.
         
-  (* returns the set of all els of x that does not belong to y *)
+  (** returns the set of all els of [x] that does not belong to [y] *)
   Fixpoint set_diff [x:set] : set -> set :=
     [y]Cases x of
     | nil => (nil A)
@@ -324,7 +324,7 @@ Section other_definitions.
 
   Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B).
 
-  (* [B^A], set of applications from [A] to [B] *)
+  (** [B^A], set of applications from [A] to [B] *)
   Definition set_power : (set A) -> (set B) -> (set (set A*B)) := 
     (list_power 1!A 2!B).
 
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 40af3d16e..37503bcef 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -20,7 +20,7 @@ Implicit Arguments On.
 Inductive list : Set := nil : list | cons : A -> list -> list.
 
 (*************************)
-(* Concatenation         *)
+(** Concatenation        *)
 (*************************)
 
 Fixpoint app [l:list] : list -> list 
@@ -140,14 +140,14 @@ Proof.
 Qed.
 
 (****************************************)
-(* Length of lists                      *)
+(** Length of lists                     *)
 (****************************************)
 
 Fixpoint length [l:list] : nat 
    := Cases l of nil => O | (cons _ m) => (S (length m)) end.
 
 (******************************)
-(* Length order of lists      *)
+(** Length order of lists     *)
 (******************************)
 
 Section length_order.
@@ -205,7 +205,7 @@ Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons
 .
 
 (*********************************)
-(* The In predicate              *)
+(** The [In] predicate           *)
 (*********************************)
 
 Fixpoint In  [a:A;l:list] : Prop :=
@@ -298,9 +298,9 @@ Proof.
 Qed.
 Hints Resolve in_or_app.
 
-(**********************)
-(* Inclusion on list  *)
-(**********************)
+(***********************)
+(** Inclusion on list  *)
+(***********************)
 Definition incl := [l,m:list](a:A)(In a l)->(In a m).
 Hints Unfold  incl.
 
@@ -373,9 +373,9 @@ Proof.
 Qed.
 Hints Resolve incl_app.
 
-(*************************)
-(* Nth element of a list *)
-(*************************)
+(**************************)
+(** Nth element of a list *)
+(**************************)
 Fixpoint nth [n:nat; l:list] : A->A :=
   [default]Cases n l of
     O (cons x l') => x
@@ -394,7 +394,7 @@ Fixpoint nth_ok [n:nat; l:list] : A->bool :=
 
 Lemma nth_in_or_default :
   (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}.
-(** Realizer nth_ok. Program_all. **)
+(* Realizer nth_ok. Program_all. *)
 Intros n l d; Generalize n; NewInduction l; Intro n0.
 Right; Case n0; Trivial.
 Case n0; Simpl.
@@ -438,8 +438,8 @@ Unfold lt; Induction l;
 ].
 i*)
 
-(* Decidable equality on lists *)
 
+(** Decidable equality on lists *)
 
 Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
 Proof.
@@ -454,7 +454,7 @@ Proof.
 Qed.
 
 (*********************************************)
-(*   Reverse Induction Principle on Lists    *)
+(**  Reverse Induction Principle on Lists    *)
 (*********************************************)
 Section Reverse_Induction.
 
@@ -546,9 +546,9 @@ Hints Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app
 
 Section Functions_on_lists.
 
-(***************************************************************)
-(* Some generic functions on lists and basic functions of them *)
-(***************************************************************)
+(****************************************************************)
+(** Some generic functions on lists and basic functions of them *)
+(****************************************************************)
 
 Section Map.
 Variables A,B:Set.
@@ -604,8 +604,8 @@ Induction l;
 ].
 Save.
 
-(* [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
-  indexed by elts of [x], sorted in lexicographic order. *)
+(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
+    indexed by elts of [x], sorted in lexicographic order. *)
 
 Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) :=
   [l']Cases l of
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
index 4e59d155d..dd7aba8c9 100644
--- a/theories/Lists/PolyListSyntax.v
+++ b/theories/Lists/PolyListSyntax.v
@@ -8,7 +8,8 @@
 
 (*i $Id$ i*)
 
-(* Syntax for list concatenation *)
+(** Syntax for list concatenation *)
+
 Require PolyList.
 
 Infix RIGHTA 7 "^" app.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 16c88e598..f5f15d889 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -58,7 +58,7 @@ Lemma Str_nth_plus
 Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes.
 Save.
 
-(* Extensional Equality between two streams  *)
+(** Extensional Equality between two streams  *)
 
 CoInductive EqSt  : Stream->Stream->Prop := 
 	    eqst : (s1,s2:Stream)
@@ -66,14 +66,14 @@ CoInductive EqSt  : Stream->Stream->Prop :=
 		   (EqSt (tl s1) (tl s2))
                     ->(EqSt s1 s2).
 
-(* A coinduction principle *)
+(** A coinduction principle *)
 
 Meta Definition CoInduction proof := 
   Cofix proof; Intros; Constructor;
     [Clear proof | Try (Apply proof;Clear proof)].
 
 
-(* Extensional equality is an equivalence relation *)
+(** Extensional equality is an equivalence relation *)
 
 Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
 (CoInduction EqSt_reflex).
@@ -99,9 +99,8 @@ Case H;  Trivial with datatypes.
 Case H0; Trivial with datatypes.
 Qed.
 
-(* 
-The definition given is equivalent to require the elements at each position to be equal 
-*)
+(** The definition given is equivalent to require the elements at each
+    position to be equal *)
 
 Theorem eqst_ntheq :
   (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2).
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index a97f54901..5a59790c0 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* Some programs and results about lists following CAML Manual *)
+(** Some programs and results about lists following CAML Manual *)
 
 Require Export PolyList.
 Set Implicit Arguments.
@@ -16,9 +16,9 @@ Chapter Lists.
 
 Variable  A : Set.
 
-(*********************)
-(* The null function *)
-(*********************)
+(**********************)
+(** The null function *)
+(**********************)
 
 Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l.
 
@@ -45,9 +45,9 @@ Program_all.
 *)
 Qed.
 
-(***********************)
-(* The Uncons function *)
-(***********************)
+(************************)
+(** The Uncons function *)
+(************************)
 
 Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}.
 Intro l; Case l.
@@ -63,7 +63,7 @@ Program_all.
 Qed.
 
 (********************************)
-(* The head function            *)
+(** The head function           *)
 (********************************)
 
 Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}.
@@ -96,7 +96,7 @@ Program_all.
 Qed.
 
 (****************************************)
-(* Length of lists                      *)
+(** Length of lists                     *)
 (****************************************)
 
 (* length is defined in PolyList *)
@@ -129,7 +129,7 @@ Program_all.
 Qed.
 
 (*******************************)
-(* Members of lists            *)
+(** Members of lists           *)
 (*******************************)
 Inductive In_spec [a:A] : (list A) -> Prop := 
    | in_hd : (l:(list A))(In_spec a (cons a l))
@@ -174,9 +174,9 @@ Program_all.
 *)
 Qed.
 
-(**********************************)
-(* Index of elements              *)
-(**********************************)
+(*********************************)
+(** Index of elements            *)
+(*********************************)
 
 Require Le.
 Require Lt.