option -dump-glob pour coqdoc

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

1 files changed, 17 insertions, 18 deletions

diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index eabcb3721..af5b04ed0 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -8,14 +8,14 @@
 
 (*i $Id$ i*)
 
-(* This module defines quantification on the world [Type] *)
-(* [Logic.v] was defining it on the world [Set] *)
+(** This module defines quantification on the world [Type]
+    ([Logic.v] was defining it on the world [Set]) *)
 
 Require Export Logic.
 Require LogicSyntax.
 
 
-(* [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
+(** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
    when [A] is of type [Type] *)
 
 Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
@@ -37,14 +37,14 @@ Qed.
 
 End universal_quantification.
 
-(* Existential Quantification *)
+(** * Existential Quantification *)
 
-(* [exT A P], or simply [(EXT x | P(x))], stands for the existential 
-   quantification on the predicate [P] when [A] is of type [Type] *)
+(** [exT A P], or simply [(EXT x | P(x))], stands for the existential 
+    quantification on the predicate [P] when [A] is of type [Type] *)
 
-(* [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the
-   existential quantification on both [P] and [Q] when [A] is of
-   type [Type] *)
+(** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the
+    existential quantification on both [P] and [Q] when [A] is of
+    type [Type] *)
 
 Inductive  exT [A:Type;P:A->Prop] : Prop
     := exT_intro : (x:A)(P x)->(exT A P).
@@ -52,8 +52,9 @@ Inductive  exT [A:Type;P:A->Prop] : Prop
 Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
     := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
 
-(* Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) *)
-(* [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of 
+(** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y)
+
+   [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of 
    type [Type]. This equality satisfies reflexivity (by definition), 
    symmetry, transitivity and stability by congruence *)
 
@@ -93,28 +94,26 @@ End Equality_is_a_congruence.
 
 Hints Immediate sym_eqT sym_not_eqT : core v62.
 
-(* This states the replacement of equals by equals in a proposition *)
+(** This states the replacement of equals by equals in a proposition *)
 
 Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
 
-(* not allowed because of dependencies:
-\begin{verbatim}
+(** not allowed because of dependencies: [[
 Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
-\end{verbatim}
-*)
+]] *)
 
-(* Some datatypes at the [Type] level *)
+(** Some datatypes at the [Type] level *)
 
 Inductive EmptyT: Type :=.
 Inductive UnitT : Type := IT : UnitT.
 
 Definition notT := [A:Type] A->EmptyT.
 
-(* Have you an idea of what means [identityT A a b] ? No matter ! *)
+(** Have you an idea of what means [identityT A a b]? No matter! *)
 
 Inductive identityT [A:Type; a:A] : A->Type :=
      refl_identityT : (identityT A a a).