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, 25 insertions, 26 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 3ddc2fc5e..b50485d3c 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -8,12 +8,12 @@
 
 (*i $Id$ i*)
 
-(*i This file formalizes Berardi's paradox which says that in
+(** This file formalizes Berardi's paradox which says that in
    the calculus of constructions, excluded middle (EM) and axiom of
    choice (AC) implie proof irrelevenace (PI).
    Here, the axiom of choice is not necessary because of the use
    of inductive types.
-
+<<
 @article{Barbanera-Berardi:JFP96,
    author    = {F. Barbanera and S. Berardi},
    title     = {Proof-irrelevance out of Excluded-middle and Choice
@@ -24,8 +24,7 @@
    number    = {3},
    pages     = {519-525}
 }
-
- i*)
+>> *)
 
 Require Elimdep.
 
@@ -33,18 +32,18 @@ Set Implicit Arguments.
 
 Section Berardis_paradox.
 
-(* Excluded middle *)
+(** Excluded middle *)
 Hypothesis EM : (P:Prop) P \/ ~P.
 
-(* Conditional on any proposition. *)
+(** Conditional on any proposition. *)
 Definition IFProp := [P,B:Prop][e1,e2:P]
   Cases (EM B) of
     (or_introl _) => e1
   | (or_intror _) => e2
   end.
 
-(* Axiom of choice applied to disjunction.
-   Provable in Coq because of dependent elimination. *)
+(** Axiom of choice applied to disjunction.
+    Provable in Coq because of dependent elimination. *)
 Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop)
   ( B -> (Q e1))->
   (~B -> (Q e2))->
@@ -56,17 +55,17 @@ Elim (EM B) using or_indd; Assumption.
 Qed.
 
 
-(* We assume a type with two elements. They play the role of booleans.
-   The main theorem under the current assumptions is that T=F *)
+(** We assume a type with two elements. They play the role of booleans.
+    The main theorem under the current assumptions is that [T=F] *)
 Variable Bool: Prop.
 Variable T: Bool.
 Variable F: Bool.
 
-(* The powerset operator *)
+(** The powerset operator *)
 Definition pow [P:Prop] :=P->Bool.
 
 
-(* A piece of theory about retracts *)
+(** A piece of theory about retracts *)
 Section Retracts.
 
 Variable A,B: Prop.
@@ -85,7 +84,7 @@ Record retract_cond : Prop := {
 
 Scheme retract_cond_indd := Induction for retract_cond Sort Prop.
 
-(* The dependent elimination above implies the axiom of choice: *)
+(** The dependent elimination above implies the axiom of choice: *)
 Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a.
 Proof.
 Intros r.
@@ -95,11 +94,11 @@ Qed.
 
 End Retracts.
 
-(* This lemma is basically a commutation of implication and existential
-   quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
-   which is provable in classical logic ( => is already provable in
-   intuitionnistic logic).
- *)
+(** This lemma is basically a commutation of implication and existential
+    quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
+    which is provable in classical logic ( => is already provable in
+    intuitionnistic logic). *)
+
 Lemma L1 : (A,B:Prop)(retract_cond (pow A) (pow B)).
 Proof.
 Intros A B.
@@ -114,10 +113,10 @@ Intros; Elim hf; Auto.
 Qed.
 
 
-(* The paradoxical set *)
+(** The paradoxical set *)
 Definition U := (P:Prop)(pow P).
 
-(* Bijection between U and (pow U) *)
+(** Bijection between [U] and [(pow U)] *)
 Definition f : U -> (pow U) :=
   [u](u U).
 
@@ -127,9 +126,9 @@ Definition g : (pow U) -> U :=
     let rU = (i2 (L1 U U)) in
     (lX (rU h)).
 
-(* We deduce that the powerset of U is a retract of U.
-   This lemma is stated in Berardi's article, but is not used
-   afterwards. *)
+(** We deduce that the powerset of [U] is a retract of [U].
+    This lemma is stated in Berardi's article, but is not used
+    afterwards. *)
 Lemma retract_pow_U_U : (retract (pow U) U).
 Proof.
 Exists g f.
@@ -140,12 +139,12 @@ Exists ([x:(pow U)]x) ([x:(pow U)]x).
 Trivial.
 Qed.
 
-(* Encoding of Russel's paradox *)
+(** Encoding of Russel's paradox *)
 
-(* The boolean negation. *)
+(** The boolean negation. *)
 Definition Not_b := [b:Bool](IFProp b==T F T).
 
-(* the set of elements not belonging not itself *)
+(** the set of elements not belonging to itself *)
 Definition R : U := (g ([u:U](Not_b (u U u)))).