summaryrefslogtreecommitdiff
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /theories/Logic
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/ConstructiveEpsilon.v6
-rw-r--r--theories/Logic/FunctionalExtensionality.v2
2 files changed, 3 insertions, 5 deletions
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 3753b97b..ff70c9fb 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
(** This module proves the constructive description schema, which
infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -14,8 +14,8 @@ predicate from the regular existence (i.e., [Prop]-existence). One
requires that the underlying set is countable and that the predicate
is decidable. *)
-(** Coq does not allow case analysis on sort [Set] when the goal is in
-[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+(** Coq does not allow case analysis on sort [Prop] when the goal is in
+[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
show [{n : nat | P n}]. However, one can perform a recursion on an
inductive predicate in sort [Prop] so that the returning type of the
recursion is in [Set]. This trick is described in Coq'Art book, Sect.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 4445b0e1..0dc82907 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -11,8 +11,6 @@
(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
-Set Manual Implicit Arguments.
-
(** The converse of functional extensionality. *)
Lemma equal_f : forall {A B : Type} {f g : A -> B},