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, 16 insertions, 17 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 2fe408543..57e93240a 100755
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -26,12 +26,12 @@ Theorem coherence_intro :  (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x
 Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)]
       (exT_intro2 A (Rstar x) (Rstar y) z h1 h2).
   
-(* A very simple case of coherence : *)
+(** A very simple case of coherence : *)
 
 Lemma Rstar_coherence : (x:A)(y:A)(Rstar x y)->(coherence x y).
  Proof  [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)).  
   
-(* coherence is symmetric *)
+(** coherence is symmetric *)
 Lemma coherence_sym: (x:A)(y:A)(coherence x y)->(coherence y x).
  Proof [x:A][y:A][h:(coherence x y)]
         (exT2_ind A (Rstar x) (Rstar y) (coherence y x)
@@ -49,30 +49,30 @@ Definition noetherian :=
   
 Section Newman_section.
 
-(* The general hypotheses of the theorem *)
+(** The general hypotheses of the theorem *)
 
 Hypothesis Hyp1:noetherian.
 Hypothesis Hyp2:(x:A)(local_confluence x).  
   
-(* The induction hypothesis *)
+(** The induction hypothesis *)
 
 Section Induct.
   Variable    x:A.
   Hypothesis  hyp_ind:(u:A)(R x u)->(confluence u).  
   
-(* Confluence in x *)
+(** Confluence in [x] *)
 
   Variables   y,z:A.  
   Hypothesis  h1:(Rstar x y).  
   Hypothesis  h2:(Rstar x z).  
   
-(* particular case x->u and u->*y   *)
+(** particular case [x->u] and [u->*y]   *)
 Section Newman_.
   Variable    u:A.  
   Hypothesis  t1:(R x u).  
   Hypothesis  t2:(Rstar u y).  
   
-(* In the usual diagram, we assume also x->v and  v->*z   *)
+(** In the usual diagram, we assume also [x->v] and [v->*z] *)
 
 Theorem Diagram : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z).
 
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5c81e2e3..7b07ac0db 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -20,7 +20,7 @@ Require Relation_Definitions.
 Require PolyList.
 Require PolyListSyntax.
 
-(* Some operators to build relations *)
+(** Some operators to build relations *)
 
 Section Transitive_Closure.
   Variable A: Set.
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index ff2e02a4b..90ab6d6c2 100755
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -8,15 +8,15 @@
 
 (*i $Id$ i*)
 
-(* Properties of a binary relation R on type A *)
+(** Properties of a binary relation [R] on type [A] *)
 
 Section Rstar.
 
 Variable A : Type.  
 Variable R : A->A->Prop.  
 
-(* Definition of the reflexive-transitive closure R* of R *)
-(* Smallest reflexive P containing R o P *)
+(** Definition of the reflexive-transitive closure [R*] of [R] *)
+(** Smallest reflexive [P] containing [R o P] *)
 
 Definition Rstar  := [x,y:A](P:A->A->Prop)
    ((u:A)(P u u))->((u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)) -> (P x y).  
@@ -32,7 +32,7 @@ Theorem Rstar_R: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z).
        [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
        (h2 x y z t1 (t2 P h1 h2)).  
   
-(* We conclude with transitivity of Rstar : *)
+(** We conclude with transitivity of [Rstar] : *)
 
 Theorem  Rstar_transitive:  (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z).
  Proof  [x:A][y:A][z:A][h:(Rstar x y)]
@@ -41,8 +41,8 @@ Theorem  Rstar_transitive:  (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z)
            ([u:A][v:A][w:A][t1:(R u v)][t2:(Rstar w z)->(Rstar v z)]
             [t3:(Rstar w z)](Rstar_R u v z t1 (t2 t3)))).  
 
-(* Another characterization of R* *)
-(* Smallest reflexive P containing R o R* *)
+(** Another characterization of [R*] *)
+(** Smallest reflexive [P] containing [R o R*] *)
 
 Definition Rstar' := [x:A][y:A](P:A->A->Prop)
     ((P x x))->((u:A)(R x u)->(Rstar u y)->(P x y)) -> (P x y).  
@@ -55,7 +55,7 @@ Theorem Rstar'_R: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y).
         [P:A->A->Prop][h1:(P x x)]
         [h2:(u:A)(R x u)->(Rstar u y)->(P x y)](h2 z t1 t2).  
   
-(* Equivalence of the two definitions: *)
+(** Equivalence of the two definitions: *)
 
 Theorem Rstar'_Rstar:  (x:A)(y:A)(Rstar' x y)->(Rstar x y).
  Proof  [x:A][y:A][h:(Rstar' x y)]
@@ -67,8 +67,7 @@ Theorem Rstar_Rstar':  (x:A)(y:A)(Rstar x y)->(Rstar' x y).
           (Rstar'_R u w v h1 (Rstar'_Rstar v w h2)))).  
 
 
-
-(* Property of Commutativity of two relations *)
+(** Property of Commutativity of two relations *)
 
 Definition commut := [A:Set][R1,R2:A->A->Prop]
                        (x,y:A)(R1 y x)->(z:A)(R2 z y)