diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index 5d867935846d46b2dd6cdd7adbc5c8a172ef82c0..fa43cb75133b8921e1f7aba0e4b36fe8afb87505 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -141,11 +141,11 @@ Proof.
   intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
   apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
-Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
+Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
 
 Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
-Hint Resolve validity_valid_car_valid : core.
+Local Hint Resolve validity_valid_car_valid : core.
 Program Instance validity_pcore : PCore (validity A) := λ x,
   Some (Validity (core (validity_car x)) (✓ x) _).
 Solve Obligations with naive_solver eauto using dra_core_valid.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 65257373f03d9a38118c3b9c0c9b94688481794a..c35d4c75dae4206a2ee613f45e2669f96ac70c4a 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -54,12 +54,12 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
   S ≫= λ s, up s T.
 
 (** Tactic setup *)
-Hint Resolve Step : core.
-Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (_ ∈ _) => set_solver : sts.
-Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-Hint Extern 50 (_ ## _) => set_solver : sts.
+Local Hint Resolve Step : core.
+Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Local Hint Extern 50 (_ ⊆ _) => set_solver : sts.
+Local Hint Extern 50 (_ ## _) => set_solver : sts.
 
 (** ** Setoids *)
 Instance frame_step_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
@@ -221,11 +221,11 @@ Instance sts_op : Op (car sts) := λ x1 x2,
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2)(* never happens *)
   end.
 
-Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (∃ s : state sts, _) => set_solver : sts.
-Hint Extern 50 (_ ∈ _) => set_solver : sts.
-Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-Hint Extern 50 (_ ## _) => set_solver : sts.
+Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (∃ s : state sts, _) => set_solver : sts.
+Local Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Local Hint Extern 50 (_ ⊆ _) => set_solver : sts.
+Local Hint Extern 50 (_ ## _) => set_solver : sts.
 
 Global Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s).
 Proof. by constructor. Qed.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 2cf522d112980c2cdb7698efa0bc945f0eccdb27..8cfae37ef79a5b20eef95f664eb6a6c5b93d7475 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -429,7 +429,7 @@ Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
 Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails : core.
+Local Hint Immediate uPred_in_entails : core.
 
 Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
 Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 8f7c63fd052680eaa36ad5d2bd4b38cb19dcda57..8dc90eaff097a2305912df4d1e107d4accff1c45 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -21,7 +21,7 @@ Implicit Types P Q R : PROP.
 Implicit Types Ps : list PROP.
 Implicit Types A : Type.
 
-Hint Extern 100 (NonExpansive _) => solve_proper : core.
+Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
 (* Force implicit argument PROP *)
 Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
@@ -95,9 +95,9 @@ Proof. intros ->; apply exist_intro. Qed.
 Lemma forall_elim' {A} P (Ψ : A → PROP) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
 Proof. move=> HP a. by rewrite HP forall_elim. Qed.
 
-Hint Resolve pure_intro forall_intro : core.
-Hint Resolve or_elim or_intro_l' or_intro_r' : core.
-Hint Resolve and_intro and_elim_l' and_elim_r' : core.
+Local Hint Resolve pure_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
+Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
 
 Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
 Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
@@ -114,7 +114,7 @@ Lemma False_elim P : False ⊢ P.
 Proof. by apply (pure_elim' False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply pure_intro. Qed.
-Hint Immediate False_elim : core.
+Local Hint Immediate False_elim : core.
 
 Lemma entails_eq_True P Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I).
 Proof.
@@ -337,7 +337,7 @@ Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
 
 
 (* BI Stuff *)
-Hint Resolve sep_mono : core.
+Local Hint Resolve sep_mono : core.
 Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'.
 Proof. by intros; apply sep_mono. Qed.
 Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'.
@@ -810,7 +810,7 @@ Section bi_affine.
 End bi_affine.
 
 (* Properties of the persistence modality *)
-Hint Resolve persistently_mono : core.
+Local Hint Resolve persistently_mono : core.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 Global Instance persistently_flip_mono' :
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 3f61a09c42a3d8d0b9f60bf5e3ce03fd3f9caa6b..798d768592490f1c6da915dade29b90b63af11b7 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -17,14 +17,14 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
 Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
-Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
 
 Global Instance later_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
 
 (* Later derived *)
-Hint Resolve later_mono : core.
+Local Hint Resolve later_mono : core.
 Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@bi_later PROP).
 Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 593d7cf7f55759216e678eb3d903e09c3e42c893..837d60c1675f2d8742546c3c6fa68a9a62c21d7e 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -85,10 +85,10 @@ Global Instance internal_eq_proper (A : ofeT) :
   Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
 
 (* Equality *)
-Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-Hint Resolve internal_eq_refl : core.
-Hint Extern 100 (NonExpansive _) => solve_proper : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+Local Hint Resolve internal_eq_refl : core.
+Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
 Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. intros ->. auto. Qed.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index bc1ca58aec67d52d9dc4fa96ae676c6cae7bc7e4..39f88ff7402025f45c6e4bd9bcbd1bcfead331af 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -121,7 +121,7 @@ Implicit Types P Q : monPred.
 
 Inductive monPred_entails (P1 P2 : monPred) : Prop :=
   { monPred_in_entails i : P1 i ⊢ P2 i }.
-Hint Immediate monPred_in_entails : core.
+Local Hint Immediate monPred_in_entails : core.
 
 Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index b8ab8b2573b96a2b8e1d8425a95715e65c80370a..aa9906ef64697b716219af18fdc4f035cf4aff5b 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -110,9 +110,9 @@ Section plainly_derived.
 Context `{BiPlainly PROP}.
 Implicit Types P : PROP.
 
-Hint Resolve pure_intro forall_intro : core.
-Hint Resolve or_elim or_intro_l' or_intro_r' : core.
-Hint Resolve and_intro and_elim_l' and_elim_r' : core.
+Local Hint Resolve pure_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
+Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
 
 Global Instance plainly_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 11372d1c7750545bf738f4381d06dce5be7713e7..016e13f4cf59abdc34dc72ffc774aa0f8c701682 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -10,10 +10,10 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Hint Resolve head_prim_reducible head_reducible_prim_step : core.
+Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
 Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
-Hint Resolve reducible_not_val_inhabitant : core.
-Hint Resolve head_stuck_stuck : core.
+Local Hint Resolve reducible_not_val_inhabitant : core.
+Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index c599f97c93ea499bb182593cad42ef426fe65913..9649a812480078e9a76a42ecc77a4e6c79f2bbe2 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -109,7 +109,7 @@ Section language.
        ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
        prim_step e1 σ1 κ e2 σ2 efs →
        step ρ1 κ ρ2.
-  Hint Constructors step : core.
+  Local Hint Constructors step : core.
 
   Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
     | nsteps_refl ρ :
@@ -118,7 +118,7 @@ Section language.
        step ρ1 κ ρ2 →
        nsteps n ρ2 κs ρ3 →
        nsteps (S n) ρ1 (κ ++ κs) ρ3.
-  Hint Constructors nsteps : core.
+  Local Hint Constructors nsteps : core.
 
   Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
 
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 9b532e703650ff8286a6d1c2082d79f7a3006ae3..04189b77f26368933be32dce59b8317189c9ec0e 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -14,7 +14,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Hint Resolve reducible_no_obs_reducible : core.
+Local Hint Resolve reducible_no_obs_reducible : core.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 9b8e438be1a5e1f2bcb549a5366ed79bc8da59e3..4c2ca48c5655670a19aaf9a9d1818691b0a09637 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -210,10 +210,10 @@ Section ectx_lifting.
   Implicit Types s : stuckness.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
-  Hint Resolve head_prim_reducible head_reducible_prim_step : core.
+  Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
   Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
-  Hint Resolve reducible_not_val_inhabitant : core.
-  Hint Resolve head_stuck_stuck : core.
+  Local Hint Resolve reducible_not_val_inhabitant : core.
+  Local Hint Resolve head_stuck_stuck : core.
 
   Lemma ownP_lift_head_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ (ownP σ1) ∗
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 2d0d1043db9ecb81b232e7cee3fbf3e56277aa9c..0f7147c5a8bb7994519d549c5c65ee51e9d2d73d 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -9,7 +9,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
+Local Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
   head_reducible_no_obs_reducible : core.
 
 Lemma twp_lift_head_step {s E Φ} e1 :
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index c1e4eb617859d4f803e99ecda46b97f82a276233..ba799dd8f494c258f104420e457c412a3f1739b8 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -11,7 +11,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Hint Resolve reducible_no_obs_reducible : core.
+Local Hint Resolve reducible_no_obs_reducible : core.
 
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index fb132f827b81ef04a9500fd0f6ce4a976f401690..02f3e6c480d97dfdc017d8c366618c32c49765bd 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -90,7 +90,7 @@ Context {A : Type}.
 Implicit Types Γ : env A.
 Implicit Types i : ident.
 Implicit Types x : A.
-Hint Resolve Esnoc_wf Enil_wf : core.
+Local Hint Resolve Esnoc_wf Enil_wf : core.
 
 Ltac simplify :=
   repeat match goal with