Fix some typos.

3 files changed, 15 insertions, 15 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index d8416b3e2..033ad1568 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -52,7 +52,7 @@ We let also
 - IPL^2   = 2nd-order functional minimal predicate logic (with ex. quant.)
 - IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.)
 
-with no prerequisite on the non-emptyness of domains
+with no prerequisite on the non-emptiness of domains
 
 Table of contents
 
@@ -96,7 +96,7 @@ Local Unset Intuition Negation Unfolding.
 
 (** Choice, reification and description schemes *)
 
-(** We make them all polymorphic. most of them have existentials as conclusion
+(** We make them all polymorphic. Most of them have existentials as conclusion
     so they require polymorphism otherwise their first application (e.g. to an
     existential in [Set]) will fix the level of [A].
 *)
@@ -340,7 +340,7 @@ Qed.
 
 (** We show that the guarded formulations of the axiom of choice
    are equivalent to their "omniscient" variant and comes from the non guarded
-   formulation in presence either of the independance of general premises
+   formulation in presence either of the independence of general premises
    or subset types (themselves derivable from subtypes thanks to proof-
    irrelevance) *)
 
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 *)
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 6896b2d57..50c8f5b18 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -11,8 +11,8 @@
 (** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to
     derive various contradictory contexts.
 
-    The file is devided in various sub-modules which all follow the
-    same structure: a section introduce the contradictory hypotheses
+    The file is divided into various sub-modules which all follow the
+    same structure: a section introduces the contradictory hypotheses
     and a theorem named [paradox] concludes the module with a proof of
     [False].
 
@@ -70,7 +70,7 @@
 
     - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
       Theory", 2001, revised 2007
-      (see http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz).
+      (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
 *)
 
 
@@ -81,9 +81,9 @@ Set Universe Polymorphism.
 (** * A modular proof of Hurkens's paradox. *)
 
 (** It relies on an axiomatisation of a shallow embedding of system U-
-    (i.e.  types of U- are interepreted by types of Coq). The
-    universes are encoding in a style, due to Martin-Löf, where they
-    are given with a set of name and a family [El:Name->Type] which
+    (i.e.  types of U- are interpreted by types of Coq). The
+    universes are encoded in a style, due to Martin-Löf, where they
+    are given by a set of names and a family [El:Name->Type] which
     interprets each name into a type. This allows the encoding of
     universe to be decoupled from Coq's universes. Dependent products
     and abstractions are similarly postulated rather than encoded as