1 files changed, 30 insertions, 24 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index b22f58dad..57a82161d 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -96,6 +96,12 @@ Local Unset Intuition Negation Unfolding.
 
 (** Choice, reification and description schemes *)
 
+(** 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].
+*)
+Set Universe Polymorphism.
+
 Section ChoiceSchemes.
 
 Variables A B :Type.
@@ -217,39 +223,39 @@ End ChoiceSchemes.
 (** Generalized schemes *)
 
 Notation RelationalChoice :=
-  (forall A B, RelationalChoice_on A B).
+  (forall A B : Type, RelationalChoice_on A B).
 Notation FunctionalChoice :=
-  (forall A B, FunctionalChoice_on A B).
+  (forall A B : Type, FunctionalChoice_on A B).
 Definition FunctionalDependentChoice :=
-  (forall A, FunctionalDependentChoice_on A).
+  (forall A : Type, FunctionalDependentChoice_on A).
 Definition FunctionalCountableChoice :=
-  (forall A, FunctionalCountableChoice_on A).
+  (forall A : Type, FunctionalCountableChoice_on A).
 Notation FunctionalChoiceOnInhabitedSet :=
-  (forall A B, inhabited B -> FunctionalChoice_on A B).
+  (forall A B : Type, inhabited B -> FunctionalChoice_on A B).
 Notation FunctionalRelReification :=
-  (forall A B, FunctionalRelReification_on A B).
+  (forall A B : Type, FunctionalRelReification_on A B).
 
 Notation GuardedRelationalChoice :=
-  (forall A B, GuardedRelationalChoice_on A B).
+  (forall A B : Type, GuardedRelationalChoice_on A B).
 Notation GuardedFunctionalChoice :=
-  (forall A B, GuardedFunctionalChoice_on A B).
+  (forall A B : Type, GuardedFunctionalChoice_on A B).
 Notation GuardedFunctionalRelReification :=
-  (forall A B, GuardedFunctionalRelReification_on A B).
+  (forall A B : Type, GuardedFunctionalRelReification_on A B).
 
 Notation OmniscientRelationalChoice :=
-  (forall A B, OmniscientRelationalChoice_on A B).
+  (forall A B : Type, OmniscientRelationalChoice_on A B).
 Notation OmniscientFunctionalChoice :=
-  (forall A B, OmniscientFunctionalChoice_on A B).
+  (forall A B : Type, OmniscientFunctionalChoice_on A B).
 
 Notation ConstructiveDefiniteDescription :=
-  (forall A, ConstructiveDefiniteDescription_on A).
+  (forall A : Type, ConstructiveDefiniteDescription_on A).
 Notation ConstructiveIndefiniteDescription :=
-  (forall A, ConstructiveIndefiniteDescription_on A).
+  (forall A : Type, ConstructiveIndefiniteDescription_on A).
 
 Notation IotaStatement :=
-  (forall A, IotaStatement_on A).
+  (forall A : Type, IotaStatement_on A).
 Notation EpsilonStatement :=
-  (forall A, EpsilonStatement_on A).
+  (forall A : Type, EpsilonStatement_on A).
 
 (** Subclassical schemes *)
 
@@ -293,7 +299,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_rel_choice :
-  forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R H) as (f,H0).
@@ -306,7 +312,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_description :
-  forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R) as [f H0].
@@ -319,10 +325,10 @@ Proof.
 Qed.
 
 Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
-  forall A B, FunctionalChoice_on A B <->
+  forall A B : Type, FunctionalChoice_on A B <->
     RelationalChoice_on A B /\ FunctionalRelReification_on A B.
 Proof.
-  intros A B; split.
+  intros A B. split.
   intro H; split;
     [ exact (funct_choice_imp_rel_choice H)
       | exact (funct_choice_imp_description H) ].
@@ -363,7 +369,7 @@ Proof.
 Qed.
 
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
-  forall A B, inhabited B -> RelationalChoice_on A B ->
+  forall A B : Type, inhabited B -> RelationalChoice_on A B ->
     IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
 Proof.
   intros A B Inh AC_rel IndPrem P R H.
@@ -375,7 +381,7 @@ Proof.
 Qed.
 
 Lemma guarded_rel_choice_imp_rel_choice :
-  forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B GAC_rel R H.
   destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
@@ -794,12 +800,13 @@ be applied on the same Type universes on both sides of the first
 Require Import Setoid.
 
 Theorem constructive_definite_descr_excluded_middle :
-  ConstructiveDefiniteDescription ->
+  (forall A : Type, ConstructiveDefiniteDescription_on A) ->
   (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
 Proof.
   intros Descr EM P.
   pose (select := fun b:bool => if b then P else ~P).
   assert { b:bool | select b } as ([|],HP).
+  red in Descr.
   apply Descr.
   rewrite <- unique_existence; split.
   destruct (EM P).
@@ -815,14 +822,13 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C; intuition auto using
+  intros FunReify EM C H. intuition auto using
     constructive_definite_descr_excluded_middle,
     (relative_non_contradiction_of_definite_descr (C:=C)).
 Qed.
 
 (**********************************************************************)
 (** * Choice => Dependent choice => Countable choice *)
-
 (* The implications below are standard *)
 
 Require Import Arith.