From 012087785dea50f33f32e0c23d7b6b4f39912a8a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Aug 2004 09:36:53 +0000
Subject: Commentaires coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6004 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Notations.v   |  4 ++--
 theories/Logic/Diaconescu.v | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 1ab6219f06..845837e480 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -8,9 +8,9 @@
 
 (*i $Id$ i*)
 
-(** These are the notations whose level and associativity is imposed by Coq *)
+(** These are the notations whose level and associativity are imposed by Coq *)
 
-(** Notations for logical connectives *)
+(** Notations for propositional connectives *)
 
 Reserved Notation "x <-> y" (at level 95, no associativity).
 Reserved Notation "x /\ y" (at level 80, right associativity).
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 73a2f3e9b7..d815b9dda7 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -97,23 +97,23 @@ Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
 intro P.
 
-(* first we exhibit the choice functional relation R *)
+(** first we exhibit the choice functional relation R *)
 destruct AC as [R H].
 
 set (class_of_true := fun b => b = true \/ P).
 set (class_of_false := fun b => b = false \/ P).
 
-(* the actual "decision": is (R class_of_true) = true or false? *)
+(** the actual "decision": is (R class_of_true) = true or false? *)
 destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
 exists true; left; reflexivity.
 destruct H0.
 
-(* the actual "decision": is (R class_of_false) = true or false? *)
+(** the actual "decision": is (R class_of_false) = true or false? *)
 destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
 exists false; left; reflexivity.
 destruct H1.
 
-(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
+(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
 right.
 intro HP.
 assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
@@ -129,7 +129,7 @@ rewrite <- H0''. reflexivity.
 rewrite Heq.
 assumption.
 
-(* cases where P is true *)
+(** cases where P is true *)
 left; assumption.
 left; assumption.
 
-- 
cgit v1.2.3