option -dump-glob pour coqdoc

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

3 files changed, 17 insertions, 41 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index e1eef4781..31e3ac447 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* A development of Treesort on Heap trees *)
+(** A development of Treesort on Heap trees *)
 
 (* G. Huet 1-9-95 uses Multiset *)
 
@@ -43,10 +43,8 @@ Inductive Tree : Set :=
       Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
 
-(*******************************************)
-(* a is lower than a Tree T if T is a Leaf *)
-(*      or T is a Node holding b>a         *)
-(*******************************************)
+(** [a] is lower than a Tree [T] if [T] is a Leaf
+    or [T] is a Node holding [b>a] *)
 
 Definition leA_Tree := [a:A; t:Tree]
  Cases t of 
@@ -68,9 +66,7 @@ Qed.
 Hints Resolve leA_Tree_Leaf leA_Tree_Node.
 
 
-(****************************)
-(*    The heap property     *)
-(****************************)
+(** The heap property *)
 
 Inductive is_heap : Tree -> Prop :=
       nil_is_heap : (is_heap Tree_Leaf)
@@ -115,13 +111,11 @@ Induction T; Auto with datatypes.
 Intros; Simpl; Apply leA_trans with b; Auto with datatypes.
 Qed.
 
-(************************************)
-(* contents of a tree as a multiset *)
-(************************************)
+(** contents of a tree as a multiset *)
 
-(* Nota Bene : In what follows the definition of SingletonBag
-   in not used. Actually, we could just take as postulate:
-   Parameter SingletonBag : A->multiset.  *)
+(** Nota Bene : In what follows the definition of SingletonBag
+    in not used. Actually, we could just take as postulate:
+    [Parameter SingletonBag : A->multiset].  *)
 
 Fixpoint  contents [t:Tree] : (multiset A) :=
  Cases t of
@@ -131,16 +125,12 @@ Fixpoint  contents [t:Tree] : (multiset A) :=
 end.
 
 
-(*******************************************************************)
-(* equivalence of two trees is equality of corresponding multisets *)
-(*******************************************************************)
+(** equivalence of two trees is equality of corresponding multisets *)
 
 Definition equiv_Tree := [t1,t2:Tree](meq (contents t1) (contents t2)).
 
 
-(***********************************)
-(* specification of heap insertion *)
-(***********************************)
+(** specification of heap insertion *)
 
 Inductive insert_spec [a:A; T:Tree] : Set :=
    insert_exist : (T1:Tree)(is_heap T1) ->
@@ -167,9 +157,7 @@ Apply low_trans with a; Auto with datatypes.
 Simpl; Apply treesort_twist2; Trivial with datatypes. 
 Qed.
 
-(*******************************)
-(* building a heap from a list *)
-(*******************************)
+(** building a heap from a list *)
 
 Inductive build_heap [l:(list A)] : Set :=
    heap_exist : (T:Tree)(is_heap T) ->
@@ -192,9 +180,7 @@ Apply meq_sym; Trivial with datatypes.
 Qed.
 
 
-(****************************)
-(* building the sorted list *)
-(****************************)
+(** building the sorted list *)
 
 Inductive flat_spec [T:Tree] : Set :=
  flat_exist : (l:(list A))(sort leA l) ->
@@ -220,9 +206,7 @@ Proof.
   Apply meq_right; Apply meq_sym; Trivial with datatypes.
 Qed.
 
-(*****************************)
-(* specification of treesort *)
-(*****************************)
+(** specification of treesort *)
 
 Theorem treesort : (l:(list A))
   {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 6b2373bf2..5bf3f6273 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -34,9 +34,7 @@ Hints Immediate eqA_dec leA_dec leA_antisym : default.
 Local emptyBag := (EmptyBag A).
 Local singletonBag := (SingletonBag eqA_dec).
 
-(**********************)
-(* contents of a list *)
-(**********************)
+(** contents of a list *)
 
 Fixpoint list_contents [l:(list A)] : (multiset A) :=
  Cases l of
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 06d35328b..77407c9ef 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -35,9 +35,7 @@ Hints Immediate eqA_dec leA_dec leA_antisym.
 Local emptyBag := (EmptyBag A).
 Local singletonBag := (SingletonBag eqA_dec).
 
-(************)
-(* lelistA  *)
-(************)
+(** [lelistA] *)
 
 Inductive lelistA [a:A] : (list A) -> Prop :=
       nil_leA : (lelistA a (nil A))
@@ -50,9 +48,7 @@ Proof.
   Intros; Inversion H; Trivial with datatypes.
 Qed.
 
-(**************************************)
-(* definition for a list to be sorted *)
-(**************************************)
+(** definition for a list to be sorted *)
 
 Inductive sort : (list A) -> Prop :=
    nil_sort : (sort (nil A))
@@ -73,9 +69,7 @@ Induction y; Auto with datatypes.
 Intros; Elim (!sort_inv a l); Auto with datatypes.
 Qed.
 
-(****************************)
-(* merging two sorted lists *)
-(****************************)
+(** merging two sorted lists *)
 
 Inductive merge_lem [l1:(list A);l2:(list A)] : Set :=
   merge_exist : (l:(list A))(sort l) ->