Fix some typos.

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 0eba49a7e..0d3c54d2d 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -113,23 +113,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_bool_subset_to_bool 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).
@@ -145,7 +145,7 @@ rewrite <- H0''. reflexivity.
 rewrite Heq.
 assumption.
 
-(** cases where P is true *)
+(* cases where P is true *)
 left; assumption.
 left; assumption.
 
@@ -154,7 +154,7 @@ Qed.
 End PredExt_RelChoice_imp_EM.
 
 (**********************************************************************)
-(** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+(** * Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
 
 (** This is an adaptation of Diaconescu's theorem, exploiting the
     form of extensionality provided by proof-irrelevance *)