diff options
Diffstat (limited to 'theories/Program/Equality.v')
| -rw-r--r-- | theories/Program/Equality.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 27e1ca84..d6f9bb9d 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. @@ -238,8 +237,8 @@ Ltac inject_left H := Ltac inject_right H := progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H. -Ltac autoinjections_left := repeat autoinjection ltac:inject_left. -Ltac autoinjections_right := repeat autoinjection ltac:inject_right. +Ltac autoinjections_left := repeat autoinjection ltac:(inject_left). +Ltac autoinjections_right := repeat autoinjection ltac:(inject_right). Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. @@ -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 |