diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 3f8f002a1eace6db214aba9ef8ea2f824e1494f7..6164660dc5362754174aeb3a165cf90fa0ff5095 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -3,11 +3,11 @@ From iris.algebra Require Export ofe monoid.
 From iris.prelude Require Import options.
 
 Class PCore (A : Type) := pcore : A → option A.
-Hint Mode PCore ! : typeclass_instances.
+Global Hint Mode PCore ! : typeclass_instances.
 Instance: Params (@pcore) 2 := {}.
 
 Class Op (A : Type) := op : A → A → A.
-Hint Mode Op ! : typeclass_instances.
+Global Hint Mode Op ! : typeclass_instances.
 Instance: Params (@op) 2 := {}.
 Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
 Notation "(â‹…)" := op (only parsing) : stdpp_scope.
@@ -20,17 +20,17 @@ Notation "(â‹…)" := op (only parsing) : stdpp_scope.
 Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : stdpp_scope.
 Notation "(≼)" := included (only parsing) : stdpp_scope.
-Hint Extern 0 (_ ≼ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≼ _) => reflexivity : core.
 Instance: Params (@included) 3 := {}.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
-Hint Mode ValidN ! : typeclass_instances.
+Global Hint Mode ValidN ! : typeclass_instances.
 Instance: Params (@validN) 3 := {}.
 Notation "✓{ n } x" := (validN n x)
   (at level 20, n at next level, format "✓{ n }  x").
 
 Class Valid (A : Type) := valid : A → Prop.
-Hint Mode Valid ! : typeclass_instances.
+Global Hint Mode Valid ! : typeclass_instances.
 Instance: Params (@valid) 2 := {}.
 Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
 
@@ -38,7 +38,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, n at next level, format "x  ≼{ n }  y") : stdpp_scope.
 Instance: Params (@includedN) 4 := {}.
-Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
+Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
 
 Section mixin.
   Local Set Primitive Projections.
@@ -93,10 +93,10 @@ Arguments cmra_validN : simpl never.
 Arguments cmra_ofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
-Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
-Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
-Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
+Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
+Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
+Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
+Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
 Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
@@ -145,32 +145,32 @@ Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
 (** * CoreId elements *)
 Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
 Arguments core_id {_} _ {_}.
-Hint Mode CoreId + ! : typeclass_instances.
+Global Hint Mode CoreId + ! : typeclass_instances.
 Instance: Params (@CoreId) 1 := {}.
 
 (** * Exclusive elements (i.e., elements that cannot have a frame). *)
 Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
 Arguments exclusive0_l {_} _ {_} _ _.
-Hint Mode Exclusive + ! : typeclass_instances.
+Global Hint Mode Exclusive + ! : typeclass_instances.
 Instance: Params (@Exclusive) 1 := {}.
 
 (** * Cancelable elements. *)
 Class Cancelable {A : cmraT} (x : A) :=
   cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
 Arguments cancelableN {_} _ {_} _ _ _ _.
-Hint Mode Cancelable + ! : typeclass_instances.
+Global Hint Mode Cancelable + ! : typeclass_instances.
 Instance: Params (@Cancelable) 1 := {}.
 
 (** * Identity-free elements. *)
 Class IdFree {A : cmraT} (x : A) :=
   id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
 Arguments id_free0_r {_} _ {_} _ _.
-Hint Mode IdFree + ! : typeclass_instances.
+Global Hint Mode IdFree + ! : typeclass_instances.
 Instance: Params (@IdFree) 1 := {}.
 
 (** * CMRAs whose core is total *)
 Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
-Hint Mode CmraTotal ! : typeclass_instances.
+Global Hint Mode CmraTotal ! : typeclass_instances.
 
 (** The function [core] returns a dummy when used on CMRAs without total
 core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
@@ -215,7 +215,7 @@ Arguments ucmra_ofe_mixin : simpl never.
 Arguments ucmra_cmra_mixin : simpl never.
 Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmraT.
-Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
+Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
 Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeO.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
@@ -239,7 +239,7 @@ Class CmraDiscrete (A : cmraT) := {
   cmra_discrete_ofe_discrete :> OfeDiscrete A;
   cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
 }.
-Hint Mode CmraDiscrete ! : typeclass_instances.
+Global Hint Mode CmraDiscrete ! : typeclass_instances.
 
 (** * Morphisms *)
 Class CmraMorphism {A B : cmraT} (f : A → B) := {
@@ -653,7 +653,7 @@ Section ucmra.
   Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
 End ucmra.
 
-Hint Immediate cmra_unit_cmra_total : core.
+Global Hint Immediate cmra_unit_cmra_total : core.
 
 (** * Properties about CMRAs with Leibniz equality *)
 Section cmra_leibniz.
@@ -1222,7 +1222,8 @@ Section prod.
 End prod.
 
 (* Registering as [Hint Extern] with new unification. *)
-Hint Extern 4 (CoreId _) => notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
+Global Hint Extern 4 (CoreId _) =>
+  notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
 
 Arguments prodR : clear implicits.
 
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/ofe.v b/iris/algebra/ofe.v
index 87f734ef5a6b1820371618a57e3ccb3337892d79..04de827cab60c5fb78f074477d35e7db27edf606 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -19,8 +19,8 @@ Notation "x ≡{ n }≡ y" := (dist n x y)
 Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
   (at level 70, n at next level, only parsing).
 
-Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
-Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
+Global Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
 Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
 Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
 
@@ -52,8 +52,8 @@ Structure ofeT := OfeT {
 }.
 Arguments OfeT _ {_ _} _.
 Add Printing Constructor ofeT.
-Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
-Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
 Arguments ofe_car : simpl never.
 Arguments ofe_equiv : simpl never.
 Arguments ofe_dist : simpl never.
@@ -96,12 +96,12 @@ Section ofe_mixin.
   Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
 End ofe_mixin.
 
-Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
+Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
 
 (** Discrete OFEs and discrete OFE elements *)
 Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
 Arguments discrete {_} _ {_} _ _.
-Hint Mode Discrete + ! : typeclass_instances.
+Global Hint Mode Discrete + ! : typeclass_instances.
 Instance: Params (@Discrete) 1 := {}.
 
 Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
@@ -125,7 +125,7 @@ Class Cofe (A : ofeT) := {
   conv_compl n c : compl c ≡{n}≡ c n;
 }.
 Arguments compl : simpl never.
-Hint Mode Cofe ! : typeclass_instances.
+Global Hint Mode Cofe ! : typeclass_instances.
 
 Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
   compl (chain_map f c) ≡ f (compl c).
@@ -258,7 +258,7 @@ Ltac solve_contractive :=
 (** Limit preserving predicates *)
 Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
   limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
-Hint Mode LimitPreserving + + ! : typeclass_instances.
+Global Hint Mode LimitPreserving + + ! : typeclass_instances.
 
 Section limit_preserving.
   Context `{Cofe A}.
@@ -716,7 +716,7 @@ Bind Scope oFunctor_scope with oFunctor.
 Class oFunctorContractive (F : oFunctor) :=
   oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Hint Mode oFunctorContractive ! : typeclass_instances.
+Global Hint Mode oFunctorContractive ! : typeclass_instances.
 
 (** Not a coercion due to the [Cofe] type class argument, and to avoid
 ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index efd07f08a1b92b7893d3ee8480681729d062613f..a04eb86920154fa59a18902664fedef0c4227cf2 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -17,18 +17,18 @@ From iris.prelude Require Import options.
 *)
 Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
 Arguments is_op {_} _ _ _ {_}.
-Hint Mode IsOp + - - - : typeclass_instances.
+Global Hint Mode IsOp + - - - : typeclass_instances.
 
 Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
 Proof. by rewrite /IsOp. Qed.
 
 Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
-Hint Mode IsOp' + ! - - : typeclass_instances.
-Hint Mode IsOp' + - ! ! : typeclass_instances.
+Global Hint Mode IsOp' + ! - - : typeclass_instances.
+Global Hint Mode IsOp' + - ! ! : typeclass_instances.
 
 Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
 Existing Instance is_op_lr | 0.
-Hint Mode IsOp'LR + ! - - : typeclass_instances.
+Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
 Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
 Proof. by rewrite /IsOp'LR /IsOp. Qed.
 
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/bi.v b/iris/base_logic/bi.v
index ad6814fb4cb4bc5726ac163da1d23a78d8596076..806f169d13de4f244e7db0999c7b43f6872c5184 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -160,7 +160,7 @@ Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
 Proof. intros P. exact: pure_intro. Qed.
 (* Also add this to the global hint database, otherwise [eauto] won't work for
 many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate uPred_affine : core.
+Global Hint Immediate uPred_affine : core.
 
 Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
 Proof. exact: @plainly_exist_1. Qed.
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 36a4fdd4f2d470afb57ca4f7d401608121d766bb..d91c4229d8b044f2498ab9a92f6ee464e02d1a78 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -88,7 +88,7 @@ search is only triggered if the arguments of [subG] do not contain evars. Since
 instance search for [subG] is restrained, instances should persistently have [subG] as
 their first parameter to avoid loops. For example, the instances [subG_authΣ]
 and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
-Hint Mode subG ! + : typeclass_instances.
+Global Hint Mode subG ! + : typeclass_instances.
 
 Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
 Proof.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 5e9faf31eaab6b9842effb3d5fd63805d4721280..49bee658b8762f75696f2bc4296301042313f9d5 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -20,7 +20,7 @@ Arguments inG_apply {_ _} _ _ {_}.
 (** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
 mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
 not want Coq to pick one arbitrarily. *)
-Hint Mode inG - ! : typeclass_instances.
+Global Hint Mode inG - ! : typeclass_instances.
 
 Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index bdb236c4e46a27b084674a053242e628666ad69f..8cfae37ef79a5b20eef95f664eb6a6c5b93d7475 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -245,7 +245,7 @@ Qed.
 (** logical entailement *)
 Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
   { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
-Hint Resolve uPred_mono : uPred_def.
+Global Hint Resolve uPred_mono : uPred_def.
 
 (** logical connectives *)
 Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
@@ -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_connectives.v b/iris/bi/derived_connectives.v
index 88e7dcca53f19f56a198e9f21662aa9da0294f45..abdfdf5961fff137c482067e1536c7ace6ae9c3f 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -16,7 +16,7 @@ Infix "∗-∗" := bi_wand_iff : bi_scope.
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
-Hint Mode Persistent + ! : typeclass_instances.
+Global Hint Mode Persistent + ! : typeclass_instances.
 Instance: Params (@Persistent) 1 := {}.
 
 Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
@@ -28,15 +28,15 @@ Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Arguments Affine {_} _%I : simpl never.
 Arguments affine {_} _%I {_}.
-Hint Mode Affine + ! : typeclass_instances.
+Global Hint Mode Affine + ! : typeclass_instances.
 
 Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Hint Mode BiAffine ! : typeclass_instances.
+Global Hint Mode BiAffine ! : typeclass_instances.
 Existing Instance absorbing_bi | 0.
 
 Class BiPositive (PROP : bi) :=
   bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
-Hint Mode BiPositive ! : typeclass_instances.
+Global Hint Mode BiPositive ! : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
@@ -47,7 +47,7 @@ Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I.
-Hint Mode Absorbing + ! : typeclass_instances.
+Global Hint Mode Absorbing + ! : typeclass_instances.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <pers> P else P)%I.
@@ -103,7 +103,7 @@ Typeclasses Opaque bi_except_0.
 Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
 Arguments Timeless {_} _%I : simpl never.
 Arguments timeless {_} _%I {_}.
-Hint Mode Timeless + ! : typeclass_instances.
+Global Hint Mode Timeless + ! : typeclass_instances.
 Instance: Params (@Timeless) 1 := {}.
 
 (** An optional precondition [mP] to [Q].
@@ -128,7 +128,7 @@ The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [B
 It is provided by the lemma [löb] in [derived_laws_later]. *)
 Class BiLöb (PROP : bi) :=
   löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
-Hint Mode BiLöb ! : typeclass_instances.
+Global Hint Mode BiLöb ! : typeclass_instances.
 Arguments löb_weak {_ _} _ _.
 
 Notation BiLaterContractive PROP :=
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/embedding.v b/iris/bi/embedding.v
index 354028caabd165472d308e02fb54b0fd1c44b8ef..c6532c19817be60a678d3a268ab3910dca90ffe8 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -12,8 +12,8 @@ Notation "⎡ P ⎤" := (embed P) : bi_scope.
 Instance: Params (@embed) 3 := {}.
 Typeclasses Opaque embed.
 
-Hint Mode Embed ! - : typeclass_instances.
-Hint Mode Embed - ! : typeclass_instances.
+Global Hint Mode Embed ! - : typeclass_instances.
+Global Hint Mode Embed - ! : typeclass_instances.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
@@ -47,43 +47,43 @@ Class BiEmbed (PROP1 PROP2 : bi) := {
   bi_embed_embed :> Embed PROP1 PROP2;
   bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
 }.
-Hint Mode BiEmbed ! - : typeclass_instances.
-Hint Mode BiEmbed - ! : typeclass_instances.
+Global Hint Mode BiEmbed ! - : typeclass_instances.
+Global Hint Mode BiEmbed - ! : typeclass_instances.
 Arguments bi_embed_embed : simpl never.
 
 Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
   embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
-Hint Mode BiEmbedEmp ! - - : typeclass_instances.
-Hint Mode BiEmbedEmp - ! - : typeclass_instances.
+Global Hint Mode BiEmbedEmp ! - - : typeclass_instances.
+Global Hint Mode BiEmbedEmp - ! - : typeclass_instances.
 
 Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
   embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤.
-Hint Mode BiEmbedLater ! - - : typeclass_instances.
-Hint Mode BiEmbedLater - ! - : typeclass_instances.
+Global Hint Mode BiEmbedLater ! - - : typeclass_instances.
+Global Hint Mode BiEmbedLater - ! - : typeclass_instances.
 
 Class BiEmbedInternalEq (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
   embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
-Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
-Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
 
 Class BiEmbedBUpd (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
   embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
-Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
-Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
 
 Class BiEmbedFUpd (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} :=
   embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤.
-Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
-Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
 
 Class BiEmbedPlainly (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
   embed_plainly (P : PROP1) : ⎡■ P⎤ ⊣⊢@{PROP2} ■ ⎡P⎤.
-Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
-Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
 
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.
@@ -315,4 +315,5 @@ End embed.
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
+Global Hint Extern 4 (Plain _) =>
+  notypeclasses refine (embed_plain _ _) : typeclass_instances.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index f3f66ba4f9fc016999aa3551268c999c779c39c4..ca25529a27cba845d3a82f1bff6c489b91ad3ebe 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -217,7 +217,7 @@ Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
 Arguments bi_persistently {PROP} _%I : simpl never, rename.
 Arguments bi_later {PROP} _%I : simpl never, rename.
 
-Hint Extern 0 (bi_entails _ _) => reflexivity : core.
+Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
 Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
 Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 4562e58717e7fde0d1f011612e4b108a647bbb60..837d60c1675f2d8742546c3c6fa68a9a62c21d7e 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -9,7 +9,7 @@ can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
 Class InternalEq (PROP : bi) :=
   internal_eq : ∀ {A : ofeT}, A → A → PROP.
 Arguments internal_eq {_ _ _} _ _ : simpl never.
-Hint Mode InternalEq ! : typeclass_instances.
+Global Hint Mode InternalEq ! : typeclass_instances.
 Instance: Params (@internal_eq) 3 := {}.
 Infix "≡" := internal_eq : bi_scope.
 Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
@@ -40,7 +40,7 @@ Class BiInternalEq (PROP : bi) := {
   bi_internal_eq_internal_eq :> InternalEq PROP;
   bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
 }.
-Hint Mode BiInternalEq ! : typeclass_instances.
+Global Hint Mode BiInternalEq ! : typeclass_instances.
 Arguments bi_internal_eq_internal_eq : simpl never.
 
 Section internal_eq_laws.
@@ -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/lib/fractional.v b/iris/bi/lib/fractional.v
index 644c47ef29330c4f3eef40004f66590acd14fca3..0c84e2778cad12298abbc3494ba4c78b12f9b2ca 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -14,10 +14,10 @@ Arguments AsFractional {_} _%I _%I _%Qp.
 
 Arguments fractional {_ _ _} _ _.
 
-Hint Mode AsFractional - + - - : typeclass_instances.
+Global Hint Mode AsFractional - + - - : typeclass_instances.
 (* To make [as_fractional_fractional] a useful instance, we have to
 allow [q] to be an evar. *)
-Hint Mode AsFractional - - + - : typeclass_instances.
+Global Hint Mode AsFractional - - + - : typeclass_instances.
 
 Section fractional.
   Context {PROP : bi}.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 1d11af00ca4a59e241a5f5ddc774d70bde891c9a..7c21a1e4bab58fddadf489ef7d01eb3633061ceb 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -7,7 +7,7 @@ Class Laterable {PROP : bi} (P : PROP) := laterable :
   P -∗ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
 Arguments Laterable {_} _%I : simpl never.
 Arguments laterable {_} _%I {_}.
-Hint Mode Laterable + ! : typeclass_instances.
+Global Hint Mode Laterable + ! : typeclass_instances.
 
 Section instances.
   Context {PROP : bi}.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index d1f047eb42a687c9efd9993f29453a18c3c3734c..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) _.
@@ -323,7 +323,7 @@ Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
   objective_at i j : P i -∗ P j.
 Arguments Objective {_ _} _%I.
 Arguments objective_at {_ _} _%I {_}.
-Hint Mode Objective + + ! : typeclass_instances.
+Global Hint Mode Objective + + ! : typeclass_instances.
 Instance: Params (@Objective) 2 := {}.
 
 (** Primitive facts that cannot be deduced from the BI structure. *)
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 4d2439693a914b185a7799e0d7eb1bc522b72220..aa9906ef64697b716219af18fdc4f035cf4aff5b 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type*".
 
 Class Plainly (A : Type) := plainly : A → A.
 Arguments plainly {A}%type_scope {_} _%I.
-Hint Mode Plainly ! : typeclass_instances.
+Global Hint Mode Plainly ! : typeclass_instances.
 Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.
 
@@ -42,7 +42,7 @@ Class BiPlainly (PROP : bi) := {
   bi_plainly_plainly :> Plainly PROP;
   bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
 }.
-Hint Mode BiPlainly ! : typeclass_instances.
+Global Hint Mode BiPlainly ! : typeclass_instances.
 Arguments bi_plainly_plainly : simpl never.
 
 Class BiPlainlyExist `{!BiPlainly PROP} :=
@@ -51,14 +51,14 @@ Class BiPlainlyExist `{!BiPlainly PROP} :=
 Arguments BiPlainlyExist : clear implicits.
 Arguments BiPlainlyExist _ {_}.
 Arguments plainly_exist_1 _ {_ _} _.
-Hint Mode BiPlainlyExist ! - : typeclass_instances.
+Global Hint Mode BiPlainlyExist ! - : typeclass_instances.
 
 Class BiPropExt `{!BiPlainly PROP, !BiInternalEq PROP} :=
   prop_ext_2 (P Q : PROP) : ■ (P ∗-∗ Q) ⊢ P ≡ Q.
 Arguments BiPropExt : clear implicits.
 Arguments BiPropExt _ {_ _}.
 Arguments prop_ext_2 _ {_ _ _} _.
-Hint Mode BiPropExt ! - - : typeclass_instances.
+Global Hint Mode BiPropExt ! - - : typeclass_instances.
 
 Section plainly_laws.
   Context `{BiPlainly PROP}.
@@ -94,7 +94,7 @@ End plainly_laws.
 Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
 Arguments Plain {_ _} _%I : simpl never.
 Arguments plain {_ _} _%I {_}.
-Hint Mode Plain + - ! : typeclass_instances.
+Global Hint Mode Plain + - ! : typeclass_instances.
 Instance: Params (@Plain) 1 := {}.
 
 Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
@@ -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 _.
@@ -644,11 +644,11 @@ apply it the instance at any node in the proof search tree.
 To avoid that, we declare it using a [Hint Immediate], so that it will
 only be used at the leaves of the proof search tree, i.e. when the
 premise of the hint can be derived from just the current context. *)
-Hint Immediate plain_persistent : typeclass_instances.
+Global Hint Immediate plain_persistent : typeclass_instances.
 
 (* Not defined using an ordinary [Instance] because the default
 [class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [coreP_persistent] for an
 example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Persistent _) =>
+Global Hint Extern 4 (Persistent _) =>
   notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 0dc792e34f873538a367d41a1a298f960954fb46..e63610cdea95cd2b0a43f0bb73344660c84c19a9 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type*".
 bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2 := {}.
-Hint Mode BUpd ! : typeclass_instances.
+Global Hint Mode BUpd ! : typeclass_instances.
 Arguments bupd {_}%type_scope {_} _%bi_scope.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
@@ -19,7 +19,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
 
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4 := {}.
-Hint Mode FUpd ! : typeclass_instances.
+Global Hint Mode FUpd ! : typeclass_instances.
 Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
@@ -82,23 +82,23 @@ Class BiBUpd (PROP : bi) := {
   bi_bupd_bupd :> BUpd PROP;
   bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
 }.
-Hint Mode BiBUpd ! : typeclass_instances.
+Global Hint Mode BiBUpd ! : typeclass_instances.
 Arguments bi_bupd_bupd : simpl never.
 
 Class BiFUpd (PROP : bi) := {
   bi_fupd_fupd :> FUpd PROP;
   bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
 }.
-Hint Mode BiFUpd ! : typeclass_instances.
+Global Hint Mode BiFUpd ! : typeclass_instances.
 Arguments bi_fupd_fupd : simpl never.
 
 Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
-Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
+Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
 Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
-Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
+Global Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
 (** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
 only make sense for affine logics. From the axioms below, one could derive
@@ -123,7 +123,7 @@ Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
     (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x
 }.
-Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
+Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
 Section bupd_laws.
   Context `{BiBUpd PROP}.
diff --git a/iris/prelude/options.v b/iris/prelude/options.v
index 22d74e4a485069bc1cc8ce71dcf386d6e840b23a..cd6d5b0f3e04d341c94030c94e7fc240882a2122 100644
--- a/iris/prelude/options.v
+++ b/iris/prelude/options.v
@@ -10,6 +10,10 @@ Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 that bullets and curly braces must be used to structure the proof. *)
 Export Set Default Goal Selector "!".
 
+(* We always annotate hints with locality ([Global] or [Local]). This enforces
+that at least global hints are annotated. *)
+Export Set Warnings "+deprecated-hint-without-locality".
+
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
 From iris.prelude Require Import options.
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/class_instances.v b/iris/proofmode/class_instances.v
index 8b5f315fbffb79d0bcb632ee3e7133b97406065c..6c2b00dcbc1fa9c232ffc5da3b289ca7cbf26454 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -14,7 +14,7 @@ created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
 [?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
 Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
 Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
-Hint Extern 0 (FromAssumption _ _ _) =>
+Global Hint Extern 0 (FromAssumption _ _ _) =>
   notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
 
 (* FIXME(Coq #6294): needs new unification *)
@@ -23,7 +23,7 @@ enable the better unification algorithm.
 See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
 Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
 Proof. by rewrite /FromExist. Qed.
-Hint Extern 0 (FromExist _ _) =>
+Global Hint Extern 0 (FromExist _ _) =>
   notypeclasses refine (from_exist_exist _) : typeclass_instances.
 
 Section class_instances.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index b71455cd7e8605a794b309a902db41a99f9e10c6..51886c557b9bc54f7610689b22bc59597fef48c6 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -9,25 +9,25 @@ Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   from_assumption : □?p P ⊢ Q.
 Arguments FromAssumption {_} _ _%I _%I : simpl never.
 Arguments from_assumption {_} _ _%I _%I {_}.
-Hint Mode FromAssumption + + - - : typeclass_instances.
+Global Hint Mode FromAssumption + + - - : typeclass_instances.
 
 Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   knownl_from_assumption :> FromAssumption p P Q.
 Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
 Arguments knownl_from_assumption {_} _ _%I _%I {_}.
-Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
+Global Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
 
 Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   knownr_from_assumption :> FromAssumption p P Q.
 Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
 Arguments knownr_from_assumption {_} _ _%I _%I {_}.
-Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
+Global Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
 
 Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
   into_pure : P ⊢ ⌜φ⌝.
 Arguments IntoPure {_} _%I _%type_scope : simpl never.
 Arguments into_pure {_} _%I _%type_scope {_}.
-Hint Mode IntoPure + ! - : typeclass_instances.
+Global Hint Mode IntoPure + ! - : typeclass_instances.
 
 (* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
 some shortcoming of unification in Coq's type class search. An example where we
@@ -53,7 +53,7 @@ Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
   into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
 Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
 Proof. by exists φ. Qed.
-Hint Extern 0 (IntoPureT _ _) =>
+Global Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
 
 (** [FromPure a P φ] is used when introducing a pure assertion. It is used by
@@ -69,27 +69,27 @@ Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
   from_pure : <affine>?a ⌜φ⌝ ⊢ P.
 Arguments FromPure {_} _ _%I _%type_scope : simpl never.
 Arguments from_pure {_} _ _%I _%type_scope {_}.
-Hint Mode FromPure + - ! - : typeclass_instances.
+Global Hint Mode FromPure + - ! - : typeclass_instances.
 
 Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
   from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure a P ψ.
 Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
   FromPure a P φ → FromPureT a P φ.
 Proof. by exists φ. Qed.
-Hint Extern 0 (FromPureT _ _ _) =>
+Global Hint Extern 0 (FromPureT _ _ _) =>
   notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
 
 Class IntoInternalEq `{BiInternalEq PROP} {A : ofeT} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
 Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
 Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
-Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
+Global Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
 
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
   into_persistent : <pers>?p P ⊢ <pers> Q.
 Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
-Hint Mode IntoPersistent + + ! - : typeclass_instances.
+Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 (** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
 a goal [P] into a modality [M] and proposition [Q].
@@ -112,7 +112,7 @@ Class FromModal {PROP1 PROP2 : bi} {A}
   from_modal : M Q ⊢ P.
 Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
 Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
-Hint Mode FromModal - + - - - ! - : typeclass_instances.
+Global Hint Mode FromModal - + - - - ! - : typeclass_instances.
 
 (** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
 proposition [Q].
@@ -122,7 +122,7 @@ Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : <affine> Q ⊢ P.
 Arguments FromAffinely {_} _%I _%I : simpl never.
 Arguments from_affinely {_} _%I _%I {_}.
-Hint Mode FromAffinely + - ! : typeclass_instances.
+Global Hint Mode FromAffinely + - ! : typeclass_instances.
 
 (** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
 the proposition [Q].
@@ -132,7 +132,7 @@ Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
   into_absorbingly : P ⊢ <absorb> Q.
 Arguments IntoAbsorbingly {_} _%I _%I.
 Arguments into_absorbingly {_} _%I _%I {_}.
-Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
+Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
 (** Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
 
@@ -146,86 +146,86 @@ Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand : □?p R ⊢ □?q P -∗ Q.
 Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
 Arguments into_wand {_} _ _ _%I _%I _%I {_}.
-Hint Mode IntoWand + + + ! - - : typeclass_instances.
+Global Hint Mode IntoWand + + + ! - - : typeclass_instances.
 
 Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand' : IntoWand p q R P Q.
 Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
-Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
-Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
+Global Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
+Global Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
 
 Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
 Arguments FromWand {_} _%I _%I _%I : simpl never.
 Arguments from_wand {_} _%I _%I _%I {_}.
-Hint Mode FromWand + ! - - : typeclass_instances.
+Global Hint Mode FromWand + ! - - : typeclass_instances.
 
 Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
 Arguments FromImpl {_} _%I _%I _%I : simpl never.
 Arguments from_impl {_} _%I _%I _%I {_}.
-Hint Mode FromImpl + ! - - : typeclass_instances.
+Global Hint Mode FromImpl + ! - - : typeclass_instances.
 
 Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
 Arguments FromSep {_} _%I _%I _%I : simpl never.
 Arguments from_sep {_} _%I _%I _%I {_}.
-Hint Mode FromSep + ! - - : typeclass_instances.
-Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
+Global Hint Mode FromSep + ! - - : typeclass_instances.
+Global Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
 
 Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
 Arguments FromAnd {_} _%I _%I _%I : simpl never.
 Arguments from_and {_} _%I _%I _%I {_}.
-Hint Mode FromAnd + ! - - : typeclass_instances.
-Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
+Global Hint Mode FromAnd + ! - - : typeclass_instances.
+Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
 Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Arguments into_and {_} _ _%I _%I _%I {_}.
-Hint Mode IntoAnd + + ! - - : typeclass_instances.
+Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
   into_sep : P ⊢ Q1 ∗ Q2.
 Arguments IntoSep {_} _%I _%I _%I : simpl never.
 Arguments into_sep {_} _%I _%I _%I {_}.
-Hint Mode IntoSep + ! - - : typeclass_instances.
+Global Hint Mode IntoSep + ! - - : typeclass_instances.
 
 Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
 Arguments FromOr {_} _%I _%I _%I : simpl never.
 Arguments from_or {_} _%I _%I _%I {_}.
-Hint Mode FromOr + ! - - : typeclass_instances.
+Global Hint Mode FromOr + ! - - : typeclass_instances.
 
 Class IntoOr {PROP : bi} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
 Arguments IntoOr {_} _%I _%I _%I : simpl never.
 Arguments into_or {_} _%I _%I _%I {_}.
-Hint Mode IntoOr + ! - - : typeclass_instances.
+Global Hint Mode IntoOr + ! - - : typeclass_instances.
 
 Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   from_exist : (∃ x, Φ x) ⊢ P.
 Arguments FromExist {_ _} _%I _%I : simpl never.
 Arguments from_exist {_ _} _%I _%I {_}.
-Hint Mode FromExist + - ! - : typeclass_instances.
+Global Hint Mode FromExist + - ! - : typeclass_instances.
 
 Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
   into_exist : P ⊢ ∃ x, Φ x.
 Arguments IntoExist {_ _} _%I _%I _ : simpl never.
 Arguments into_exist {_ _} _%I _%I _ {_}.
-Hint Mode IntoExist + - ! - - : typeclass_instances.
+Global Hint Mode IntoExist + - ! - - : typeclass_instances.
 
 Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   into_forall : P ⊢ ∀ x, Φ x.
 Arguments IntoForall {_ _} _%I _%I : simpl never.
 Arguments into_forall {_ _} _%I _%I {_}.
-Hint Mode IntoForall + - ! - : typeclass_instances.
+Global Hint Mode IntoForall + - ! - : typeclass_instances.
 
 Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
   from_forall : (∀ x, Φ x) ⊢ P.
 Arguments FromForall {_ _} _%I _%I _ : simpl never.
 Arguments from_forall {_ _} _%I _%I _ {_}.
-Hint Mode FromForall + - ! - - : typeclass_instances.
+Global Hint Mode FromForall + - ! - - : typeclass_instances.
 
 Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
 Arguments IsExcept0 {_} _%I : simpl never.
 Arguments is_except_0 {_} _%I {_}.
-Hint Mode IsExcept0 + ! : typeclass_instances.
+Global Hint Mode IsExcept0 + ! : typeclass_instances.
 
 (** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
 
@@ -250,7 +250,7 @@ Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
 Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
 Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
-Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
+Global Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
 
 (* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
 add a modality to the goal corresponding to a premise/asserted proposition. *)
@@ -258,7 +258,7 @@ Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
   add_modal : P ∗ (P' -∗ Q) ⊢ Q.
 Arguments AddModal {_} _%I _%I _%I : simpl never.
 Arguments add_modal {_} _%I _%I _%I {_}.
-Hint Mode AddModal + - ! ! : typeclass_instances.
+Global Hint Mode AddModal + - ! ! : typeclass_instances.
 
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
@@ -279,7 +279,7 @@ Proof. done. Qed.
 Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
 Arguments Frame {_} _ _%I _%I _%I.
 Arguments frame {_} _ _%I _%I _%I {_}.
-Hint Mode Frame + + ! ! - : typeclass_instances.
+Global Hint Mode Frame + + ! ! - : typeclass_instances.
 
 (* The boolean [progress] indicates whether actual framing has been performed.
 If it is [false], then the default instance [maybe_frame_default] below has been
@@ -288,7 +288,7 @@ Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
   maybe_frame : □?p R ∗ Q ⊢ P.
 Arguments MaybeFrame {_} _ _%I _%I _%I _.
 Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
-Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
+Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
 
 Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
   Frame p R P Q → MaybeFrame p R P Q true.
@@ -313,106 +313,106 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Arguments MakeEmbed {_ _ _} _%I _%I.
-Hint Mode MakeEmbed + + + - - : typeclass_instances.
+Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
 Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   known_make_embed :> MakeEmbed P Q.
 Arguments KnownMakeEmbed {_ _ _} _%I _%I.
-Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
+Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
 
 Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
 Arguments MakeSep {_} _%I _%I _%I.
-Hint Mode MakeSep + - - - : typeclass_instances.
+Global Hint Mode MakeSep + - - - : typeclass_instances.
 Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_sep :> MakeSep P Q PQ.
 Arguments KnownLMakeSep {_} _%I _%I _%I.
-Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
 Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
   knownr_make_sep :> MakeSep P Q PQ.
 Arguments KnownRMakeSep {_} _%I _%I _%I.
-Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
 
 Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
 Arguments MakeAnd {_} _%I _%I _%I.
-Hint Mode MakeAnd + - - - : typeclass_instances.
+Global Hint Mode MakeAnd + - - - : typeclass_instances.
 Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_and :> MakeAnd P Q PQ.
 Arguments KnownLMakeAnd {_} _%I _%I _%I.
-Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
 Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
   knownr_make_and :> MakeAnd P Q PQ.
 Arguments KnownRMakeAnd {_} _%I _%I _%I.
-Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
 
 Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
 Arguments MakeOr {_} _%I _%I _%I.
-Hint Mode MakeOr + - - - : typeclass_instances.
+Global Hint Mode MakeOr + - - - : typeclass_instances.
 Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_or :> MakeOr P Q PQ.
 Arguments KnownLMakeOr {_} _%I _%I _%I.
-Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
 Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
 Arguments KnownRMakeOr {_} _%I _%I _%I.
-Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
 
 Class MakeAffinely {PROP : bi} (P Q : PROP) :=
   make_affinely : <affine> P ⊣⊢ Q.
 Arguments MakeAffinely {_} _%I _%I.
-Hint Mode MakeAffinely + - - : typeclass_instances.
+Global Hint Mode MakeAffinely + - - : typeclass_instances.
 Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
   known_make_affinely :> MakeAffinely P Q.
 Arguments KnownMakeAffinely {_} _%I _%I.
-Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
+Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
 
 Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
   make_intuitionistically : □ P ⊣⊢ Q.
 Arguments MakeIntuitionistically {_} _%I _%I.
-Hint Mode MakeIntuitionistically + - - : typeclass_instances.
+Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
 Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
   known_make_intuitionistically :> MakeIntuitionistically P Q.
 Arguments KnownMakeIntuitionistically {_} _%I _%I.
-Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
+Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
 
 Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
   make_absorbingly : <absorb> P ⊣⊢ Q.
 Arguments MakeAbsorbingly {_} _%I _%I.
-Hint Mode MakeAbsorbingly + - - : typeclass_instances.
+Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
 Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
   known_make_absorbingly :> MakeAbsorbingly P Q.
 Arguments KnownMakeAbsorbingly {_} _%I _%I.
-Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
+Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
 
 Class MakePersistently {PROP : bi} (P Q : PROP) :=
   make_persistently : <pers> P ⊣⊢ Q.
 Arguments MakePersistently {_} _%I _%I.
-Hint Mode MakePersistently + - - : typeclass_instances.
+Global Hint Mode MakePersistently + - - : typeclass_instances.
 Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
   known_make_persistently :> MakePersistently P Q.
 Arguments KnownMakePersistently {_} _%I _%I.
-Hint Mode KnownMakePersistently + ! - : typeclass_instances.
+Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
 
 Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
   make_laterN : ▷^n P ⊣⊢ lP.
 Arguments MakeLaterN {_} _%nat _%I _%I.
-Hint Mode MakeLaterN + + - - : typeclass_instances.
+Global Hint Mode MakeLaterN + + - - : typeclass_instances.
 Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
   known_make_laterN :> MakeLaterN n P lP.
 Arguments KnownMakeLaterN {_} _%nat _%I _%I.
-Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
+Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
 
 Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
   make_except_0 : ◇ P ⊣⊢ Q.
 Arguments MakeExcept0 {_} _%I _%I.
-Hint Mode MakeExcept0 + - - : typeclass_instances.
+Global Hint Mode MakeExcept0 + - - : typeclass_instances.
 Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
   known_make_except_0 :> MakeExcept0 P Q.
 Arguments KnownMakeExcept0 {_} _%I _%I.
-Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
+Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
 
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Arguments IntoExcept0 {_} _%I _%I : simpl never.
 Arguments into_except_0 {_} _%I _%I {_}.
-Hint Mode IntoExcept0 + ! - : typeclass_instances.
-Hint Mode IntoExcept0 + - ! : typeclass_instances.
+Global Hint Mode IntoExcept0 + ! - : typeclass_instances.
+Global Hint Mode IntoExcept0 + - ! : typeclass_instances.
 
 (* The class [MaybeIntoLaterN] has only two instances:
 
@@ -452,12 +452,12 @@ Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
   maybe_into_laterN : P ⊢ ▷^n Q.
 Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
 Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
-Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
+Global Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
 
 Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
   into_laterN :> MaybeIntoLaterN only_head n P Q.
 Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
-Hint Mode IntoLaterN + + + ! - : typeclass_instances.
+Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
 
 Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
   MaybeIntoLaterN only_head n P P | 1000.
@@ -477,7 +477,7 @@ Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :
   into_embed : P ⊢ ⎡Q⎤.
 Arguments IntoEmbed {_ _ _} _%I _%I.
 Arguments into_embed {_ _ _} _%I _%I {_}.
-Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
+Global Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
 
 (* We use two type classes for [AsEmpValid], in order to avoid loops in
    typeclass search. Indeed, the [as_emp_valid_embed] instance would try
@@ -510,7 +510,7 @@ Proof. by apply as_emp_valid. Qed.
    Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
 Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
-Hint Mode IntoInv + ! - : typeclass_instances.
+Global Hint Mode IntoInv + ! - : typeclass_instances.
 
 (** Accessors.
     This definition only exists for the purpose of the proof mode; a truly
@@ -533,7 +533,7 @@ Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
   elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
 Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
-Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
+Global Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
 
 (* Turn [P] into an accessor.
    Inputs:
@@ -550,7 +550,7 @@ Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
   into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
 Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
-Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
+Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 
 (* The typeclass used for the [iInv] tactic.
    Input: [Pinv]
@@ -578,7 +578,7 @@ Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
   elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
 Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
-Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
+Global Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
 
 (** We make sure that tactics that perform actions on *specific* hypotheses or
 parts of the goal look through the [tc_opaque] connective, which is used to make
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
diff --git a/iris/proofmode/ident_name.v b/iris/proofmode/ident_name.v
index 709205e3e2082d41de2c355dd40d9fcb71710019..2457b844face4062856383fd5530241f3d137d64 100644
--- a/iris/proofmode/ident_name.v
+++ b/iris/proofmode/ident_name.v
@@ -37,4 +37,4 @@ Ltac solve_as_ident_name :=
   | _ => notypeclasses refine (to_ident_name __unknown)
   end.
 
-Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
+Global Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 47127e687024fd9ad9da4d2e00340d944ac6c1c7..af764cb9e285ece79c6749bb1d9f22e4970cc3cc 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1994,7 +1994,7 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
 (** * Destruct tactic *)
 Class CopyDestruct {PROP : bi} (P : PROP).
 Arguments CopyDestruct {_} _%I.
-Hint Mode CopyDestruct + ! : typeclass_instances.
+Global Hint Mode CopyDestruct + ! : typeclass_instances.
 
 Instance copy_destruct_forall {PROP : bi} {A} (Φ : A → PROP) : CopyDestruct (∀ x, Φ x) := {}.
 Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
@@ -3261,54 +3261,54 @@ Tactic Notation "iAccu" :=
   iStartProof; eapply tac_accu; [pm_reflexivity || fail "iAccu: not an evar"].
 
 (** Automation *)
-Hint Extern 0 (_ ⊢ _) => iStartProof : core.
-Hint Extern 0 (⊢ _) => iStartProof : core.
+Global Hint Extern 0 (_ ⊢ _) => iStartProof : core.
+Global Hint Extern 0 (⊢ _) => iStartProof : core.
 
 (* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
-Hint Extern 0 (envs_entails _ ?Q) =>
+Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
+Global Hint Extern 0 (envs_entails _ ?Q) =>
   first [is_evar Q; fail 1|iAssumption] : core.
-Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
+Global Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
 
 (* TODO: look for a more principled way of adding trivial hints like those
 below; see the discussion in !75 for further details. *)
-Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
+Global Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply internal_eq_refl : core.
-Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepL_nil' _) : core.
-Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepL2_nil' _) : core.
-Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepM_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepM2_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepS_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
   rewrite envs_entails_eq; apply (big_sepMS_empty' _) : core.
 
 (* These introduce as much as possible at once, for better performance. *)
-Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
-Hint Extern 0 (envs_entails _ (_ → _)) => iIntros : core.
-Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (_ → _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros : core.
 (* Multi-intro doesn't work for custom binders. *)
-Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
-
-Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
-Hint Extern 1 (envs_entails _ (â–  _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (â–¡ _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.
-Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.
-Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft : core.
-Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight : core.
-Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.
-Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.
-
-Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
+Global Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
+
+Global Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
+Global Hint Extern 1 (envs_entails _ (â–  _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (â–¡ _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.
+Global Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.
+Global Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft : core.
+Global Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight : core.
+Global Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.
+Global Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.
+
+Global Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index f59f09245a46da1b9618fd3d39cf9e93765e7134..0b6b1df2f4e1d1790d193043795e9854e46ce6c1 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -10,13 +10,13 @@ Arguments MakeMonPredAt {_ _} _ _%I _%I.
 (** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
 proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
 important to use the mode [!] also for the first two arguments. *)
-Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
+Global Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
 
 Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
-Hint Mode IsBiIndexRel + - - : typeclass_instances.
+Global Hint Mode IsBiIndexRel + - - : typeclass_instances.
 Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
 Proof. by rewrite /IsBiIndexRel. Qed.
-Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
+Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
 (** Frame [𝓡] into the goal [monPred_at P i] and determine the remainder [𝓠].
@@ -25,7 +25,7 @@ Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
       (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP) :=
   frame_monPred_at : □?p 𝓡 ∗ 𝓠 -∗ P i.
 Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
-Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
+Global Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
 
 Section modalities.
   Context {I : biIndex} {PROP : bi}.
@@ -537,17 +537,17 @@ End bi.
 
    As a result, depending on P and Q being evars, we use a different
    version of [into_wand_monPred_at_xx_xx]. *)
-Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
+Global Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
      is_evar P; is_evar Q;
      eapply @into_wand_monPred_at_unknown_unknown
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
      eapply @into_wand_monPred_at_unknown_known
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
      eapply @into_wand_monPred_at_known_unknown_le
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
      eapply @into_wand_monPred_at_known_unknown_ge
      : typeclass_instances.
 
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index dc8be0254f5409df314fbe055b779af1ca3c18f5..375630f1d315c35fc0672c5c6af45b3821b42d0f 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -163,7 +163,7 @@ Global Instance siProp_affine : BiAffine siPropI | 0.
 Proof. intros P. exact: pure_intro. Qed.
 (* Also add this to the global hint database, otherwise [eauto] won't work for
 many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate siProp_affine : core.
+Global Hint Immediate siProp_affine : core.
 
 Global Instance siProp_plain (P : siProp) : Plain P | 0.
 Proof. done. Qed.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 345994a211c472d5b5643c68c0ccca3d8b4879bd..f47bbc7d016256b53885091f8279ef31a2c38008 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -53,7 +53,7 @@ End cofe.
 (** logical entailement *)
 Inductive siProp_entails (P Q : siProp) : Prop :=
   { siProp_in_entails : ∀ n, P n → Q n }.
-Hint Resolve siProp_closed : siProp_def.
+Global Hint Resolve siProp_closed : siProp_def.
 
 (** logical connectives *)
 Program Definition siProp_pure_def (φ : Prop) : siProp :=
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 36deec1e87495d631f0525283e756acff936e750..1caa7591696f623babe3b781ba4c7cbf9d4061be 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -169,9 +169,9 @@ To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
 behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
 Class AsRecV (v : val) (f x : binder) (erec : expr) :=
   as_recv : v = RecV f x erec.
-Hint Mode AsRecV ! - - - : typeclass_instances.
+Global Hint Mode AsRecV ! - - - : typeclass_instances.
 Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
-Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
+Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
   apply AsRecV_recv : typeclass_instances.
 
 Instance pure_recc f x (erec : expr) :