summaryrefslogtreecommitdiff
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
commitde0085539583f59dc7c4bf4e272e18711d565466 (patch)
tree347e1d95a2df56f79a01b303e485563588179e91 /theories/Logic
parente978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff)
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/ChoiceFacts.v10
-rw-r--r--theories/Logic/ClassicalUniqueChoice.v6
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.