3 files changed, 6 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3e282f696a..3ecb5a5a61 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,6 +26,7 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
+#[global]
 Hint Unfold compose : core.
 
 Declare Scope program_scope.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 5862a08838..25af2d5ffb 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -21,6 +21,7 @@ Ltac is_ground_goal :=
 
 (** Try to find a contradiction. *)
 
+#[global]
 Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 
 (** We will use the [block] definition to separate the goal from the 
@@ -308,6 +309,7 @@ Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 (** This hint database and the following tactic can be used with [autounfold] to 
    unfold everything to [eq_rect]s. *)
 
+#[global]
 Hint Unfold solution_left solution_right deletion simplification_heq
   simplification_existT1 simplification_existT2 simplification_K
   eq_rect_r eq_rec eq_ind : dep_elim.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 50351d6a14..d1be8812e9 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -12,8 +12,6 @@
 
 Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
-Require Import ProofIrrelevance.
-Require Import FunctionalExtensionality.
 
 Local Open Scope program_scope.
 
@@ -51,7 +49,7 @@ Section Well_founded.
   Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
   Proof.
     intro x; induction (Rwf x); intros.
-    rewrite (proof_irrelevance (Acc R x) r s) ; auto.
+    rewrite <- 2 Fix_F_eq; intros. apply F_ext; intros []; auto.
   Qed.
 
   Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
@@ -110,6 +108,7 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
+#[global]
 Hint Resolve measure_wf : core.
 
 Section Fix_rects.
@@ -226,6 +225,7 @@ Ltac fold_sub f :=
 
 (** This module provides the fixpoint equation provided one assumes
    functional extensionality. *)
+Require Import FunctionalExtensionality.
 
 Module WfExtensionality.