Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index e0be9ed3..d2b7db04 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ChoiceFacts.v 8999 2006-07-04 12:46:04Z notin $ i*)
 
 (** ** Some facts and definitions concerning choice and description in
        intuitionistic logic.
@@ -78,7 +78,7 @@ unpublished.
 [Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
-[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
 intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
@@ -125,7 +125,7 @@ Definition FunctionalRelReification_on :=
 
 (** ID_epsilon (constructive version of indefinite description;
     combined with proof-irrelevance, it may be connected to
-    Carlstrøm's type theory with a constructive indefinite description
+    Carlstrøm's type theory with a constructive indefinite description
     operator) *)
 
 Definition ConstructiveIndefiniteDescription_on :=
@@ -133,7 +133,7 @@ Definition ConstructiveIndefiniteDescription_on :=
   (exists x, P x) -> { x:A | P x }.
 
 (** ID_iota (constructive version of definite description; combined
-    with proof-irrelevance, it may be connected to Carlstrøm's and
+    with proof-irrelevance, it may be connected to Carlstrøm's and
     Stenlund's type theory with a constructive definite description
     operator) *)
 
@@ -694,7 +694,7 @@ Qed.
     We adapt the proof to show that constructive definite description
     transports excluded-middle from [Prop] to [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 79bef2af..28d32fcc 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalUniqueChoice.v 8893 2006-06-04 18:04:53Z herbelin $ i*)
+(*i $Id: ClassicalUniqueChoice.v 9026 2006-07-06 15:16:20Z herbelin $ i*)
 
 (** This file provides classical logic and unique choice *)
 
@@ -15,7 +15,7 @@
     excluded-middle in [Set], hence it implies a strongly classical
     world. Especially it conflicts with the impredicativity of [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
@@ -39,7 +39,7 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The followig proof comes from [ChicliPottierSimpson02] *)
+(** The following proof comes from [ChicliPottierSimpson02] *)
 
 Require Import Setoid.