From 6d3adf8452bd953fa88e7015261fa006f0dea157 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 11:25:59 +0200
Subject: [PATCH] remove legacy hint db entries

---
 theories/base_logic/base_logic.v |  9 ---------
 theories/base_logic/lib/own.v    |  2 +-
 theories/bi/bi.v                 | 11 -----------
 theories/proofmode/coq_tactics.v |  2 +-
 4 files changed, 2 insertions(+), 22 deletions(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 3fd684dca..40a3d9a3e 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -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}.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index b87d8491f..a2bdd3d2e 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -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 *)
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 95fbe03a9..9e9de7dba 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -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.
-*)
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ad4e9c349..444dd0a8d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -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 :
-- 
GitLab