Commit 6d3adf84 authored by Ralf Jung's avatar Ralf Jung

remove legacy hint db entries

parent 54d2fa74
......@@ -12,15 +12,6 @@ Module Import uPred.
Export bi.
End uPred.
(* Hint DB for the logic *)
Hint Resolve pure_intro : I.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve persistently_mono : I.
Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r' *)
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl internal_eq_refl : I.
(* Setup of the proof mode *)
Section class_instances.
Context {M : ucmraT}.
......
......@@ -128,7 +128,7 @@ Qed.
Lemma own_alloc a : a (|==> γ, own γ a)%I.
Proof.
intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_strong a ) //; [].
apply bupd_mono, exist_mono=>?. eauto with I.
apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
Qed.
(** ** Frame preserving updates *)
......
......@@ -7,14 +7,3 @@ Module Import bi.
Export bi.derived_laws_bi.bi.
Export bi.derived_laws_sbi.bi.
End bi.
(* Hint DB for the logic *)
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
Hint Resolve and_intro and_elim_l' and_elim_r' : BI.
Hint Resolve persistently_mono : BI.
Hint Resolve sep_elim_l sep_elim_r sep_mono : BI.
Hint Immediate True_intro False_elim : BI.
(*
Hint Immediate iff_refl internal_eq_refl' : BI.
*)
......@@ -832,7 +832,7 @@ Lemma tac_specialize_persistent_helper_done Δ i q P :
envs_entails Δ (<absorb> P).
Proof.
rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
rewrite intuitionistically_if_elim comm. f_equiv; auto.
rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment