Commentaires coqdoc

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

3 files changed, 12 insertions, 12 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 933761612..f7a38cd02 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -8,12 +8,12 @@
 
 (*i $Id$ i*)
 
-(* We show that the functional formulation of the axiom of Choice
+(** We show that the functional formulation of the axiom of Choice
    (usual formulation in type theory) is equivalent to its relational
    formulation (only formulation of set theory) + the axiom of
    (parametric) definite description (aka axiom of unique choice) *)
 
-(* This shows that the axiom of choice can be assumed (under its
+(** This shows that the axiom of choice can be assumed (under its
    relational formulation) without known inconsistency with classical logic,
    though definite description conflicts with classical logic *)
 
@@ -80,7 +80,7 @@ intro H; split;
 intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
-(* We show that the guarded relational formulation of the axiom of Choice
+(** We show that the guarded relational formulation of the axiom of Choice
    comes from the non guarded formulation in presence either of the
    independance of premises or proof-irrelevance *)
 
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 095e53caa..73a2f3e9b 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
+(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
    entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
    adapted the proof to show that the axiom of choice in equivalence
    classes entails Excluded-Middle in Type Theory.
@@ -27,12 +27,12 @@
 
 Section PredExt_GuardRelChoice_imp_EM.
 
-(* The axiom of extensionality for predicates *)
+(** The axiom of extensionality for predicates *)
 
 Definition PredicateExtensionality :=
   forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
 
-(* From predicate extensionality we get propositional extensionality
+(** From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
 Require Import ClassicalFacts.
@@ -54,7 +54,7 @@ Proof.
   apply (ext_prop_dep_proof_irrel_cic prop_ext).
 Qed.
 
-(* From proof-irrelevance and relational choice, we get guarded
+(** From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
 Require Import ChoiceFacts.
@@ -73,8 +73,8 @@ Proof.
    (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
 Qed.
 
-(* The form of choice we need: there is a functional relation which chooses
-   an element in any non empty subset of bool *)
+(** The form of choice we need: there is a functional relation which chooses
+    an element in any non empty subset of bool *)
 
 Require Import Bool.
 
@@ -90,8 +90,8 @@ Proof.
   exact (fun _ H => H).
 Qed.
 
-(* The proof of the excluded middle *)
-(* Remark: P could have been in Set or Type *)
+(** The proof of the excluded middle *)
+(** Remark: P could have been in Set or Type *)
 
 Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 5b847c785..feb11b827 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* This file axiomatizes the relational form of the axiom of choice *)
+(** This file axiomatizes the relational form of the axiom of choice *)
 
 Axiom
   relational_choice :