Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

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},