diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 3fd684dca77f12ab43105b1e7c0731ce9202e79e..40a3d9a3eea6dde15f21c9faa89123226605d00e 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 b87d8491ff85e8eff241f39a59739d3bd52f6eb5..a2bdd3d2e073017132e306078a23ac8a5d461ee7 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 95fbe03a91bea11f7685a5698cd1ffe727f59ae3..9e9de7dbae24213b688f9705816f74f5d8fd6415 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 ad4e9c3496ade97904144cabbdfe890ec791cb0f..444dd0a8dc9c94b38606f72829eb50527b61269f 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 :