4 files changed, 6 insertions, 6 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 17f05c5113..d6f9bb9df0 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -8,7 +8,6 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-Require Export ProofIrrelevance.
 Require Export JMeq.
 
 Require Import Coq.Program.Tactics.
@@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p :=
       | [ H : X = Y |- _ ] =>
         match p with
           | H => fail 2
-          | _ => rewrite (proof_irrelevance (X = Y) p H)
+          | _ => rewrite (UIP _ X Y p H)
         end
       | _ => fail " No hypothesis with same type "
     end
@@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id.
    [coerce_* t eq_refl = t]. *)
 
 Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
-Proof. apply proof_irrelevance. Qed.
+Proof. apply UIP. Qed.
 
 Lemma UIP_refl_refl A (x : A) :
   Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
@@ -333,7 +332,7 @@ Ltac simplify_one_dep_elim_term c :=
       (let hyp := fresh in intros hyp ;
         move hyp before y ; revert_until hyp ; generalize dependent y ;
           refine (solution_right _ _ _ _)(*  ; intros until 0 *))
-    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c8f37318d1..2a3ec926b2 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,7 @@
 
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
+Require Export ProofIrrelevance.
 
 Local Open Scope program_scope.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 7384790dae..dfd6b0eae0 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -264,7 +264,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | appcontext [False_rect _ ?p] => elim p
+        | context [False_rect _ ?p] => elim p
       end
   end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a2fd05cd96..c490ea5166 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end