3 files changed, 7 insertions, 5 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 22436de69..ab1eccee2 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -15,6 +15,8 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
+Set Universe Polymorphism.
+
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
 Arguments id {A} x.
@@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
 
 (** The [flip] combinator reverses the first two arguments of a function. *)
 
-Definition flip {A B C} (f : A -> B -> C) x y := f y x.
+Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
 (** Application as a combinator. *)
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 323e80cc3..96345e154 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -263,7 +263,7 @@ Class DependentEliminationPackage (A : Type) :=
 
 Ltac elim_tac tac p :=
   let ty := type of p in
-  let eliminator := eval simpl in (elim (A:=ty)) in
+  let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in
     tac p eliminator.
 
 (** Specialization to do case analysis or induction.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index f6d795b94..d82fa602a 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -153,7 +153,7 @@ Section Fix_rects.
 
   Hypothesis equiv_lowers:
     forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
-    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) ->
+    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) ->
       f g = f h.
 
   (* From equiv_lowers, it follows that
@@ -231,10 +231,10 @@ Module WfExtensionality.
   Program Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
-      (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x),
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y).
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)).
   Proof.
     intros ; apply Fix_eq ; auto.
     intros.