diff --git a/theories/base.v b/theories/base.v
index f7c8dac003818328e4cdf85784b9da7ef37c4560..c1fa499aabd67cfbc18e34f346daad88ef06f511 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -71,7 +71,7 @@ issue #6714.
 See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
 of this type class. *)
 Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
-Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
+Global Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
 
 (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
 as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
@@ -83,7 +83,7 @@ Inductive TCIf (P Q R : Prop) : Prop :=
   | TCIf_false : R → TCIf P Q R.
 Existing Class TCIf.
 
-Hint Extern 0 (TCIf _ _ _) =>
+Global Hint Extern 0 (TCIf _ _ _) =>
   first [apply TCIf_true; [apply _|]
         |apply TCIf_false] : typeclass_instances.
 
@@ -116,12 +116,12 @@ Inductive TCOr (P1 P2 : Prop) : Prop :=
 Existing Class TCOr.
 Existing Instance TCOr_l | 9.
 Existing Instance TCOr_r | 10.
-Hint Mode TCOr ! ! : typeclass_instances.
+Global Hint Mode TCOr ! ! : typeclass_instances.
 
 Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
 Existing Class TCAnd.
 Existing Instance TCAnd_intro.
-Hint Mode TCAnd ! ! : typeclass_instances.
+Global Hint Mode TCAnd ! ! : typeclass_instances.
 
 Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
@@ -133,7 +133,7 @@ Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
 Existing Class TCForall.
 Existing Instance TCForall_nil.
 Existing Instance TCForall_cons.
-Hint Mode TCForall ! ! ! : typeclass_instances.
+Global Hint Mode TCForall ! ! ! : typeclass_instances.
 
 (** The class [TCForall2 P l k] is commonly used to transform an input list [l]
 into an output list [k], or the converse. Therefore there are two modes, either
@@ -145,8 +145,8 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
 Existing Class TCForall2.
 Existing Instance TCForall2_nil.
 Existing Instance TCForall2_cons.
-Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
-Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
+Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
+Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
 
 Inductive TCElemOf {A} (x : A) : list A → Prop :=
   | TCElemOf_here xs : TCElemOf x (x :: xs)
@@ -154,7 +154,7 @@ Inductive TCElemOf {A} (x : A) : list A → Prop :=
 Existing Class TCElemOf.
 Existing Instance TCElemOf_here.
 Existing Instance TCElemOf_further.
-Hint Mode TCElemOf ! ! ! : typeclass_instances.
+Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
 
 (** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
 [TCEq] can also be used to unify evars. This is harmless: since the only
@@ -163,7 +163,7 @@ https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
 Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
 Existing Instance TCEq_refl.
-Hint Mode TCEq ! - - : typeclass_instances.
+Global Hint Mode TCEq ! - - : typeclass_instances.
 
 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
 Proof. split; destruct 1; reflexivity. Qed.
@@ -172,8 +172,8 @@ Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
 Existing Instance TCDiag_diag.
-Hint Mode TCDiag ! ! ! - : typeclass_instances.
-Hint Mode TCDiag ! ! - ! : typeclass_instances.
+Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
+Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
 
 (** Given a proposition [P] that is a type class, [tc_to_bool P] will return
 [true] iff there is an instance of [P]. It is often useful in Ltac programming,
@@ -215,8 +215,8 @@ Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
 Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
   (at level 70, only parsing, no associativity) : stdpp_scope.
 
-Hint Extern 0 (_ = _) => reflexivity : core.
-Hint Extern 100 (_ ≠ _) => discriminate : core.
+Global Hint Extern 0 (_ = _) => reflexivity : core.
+Global Hint Extern 100 (_ ≠ _) => discriminate : core.
 
 Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
@@ -227,7 +227,7 @@ Proof. split; repeat intro; congruence. Qed.
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
 (* No Hint Mode set because of Coq bug #5735
-Hint Mode Equiv ! : typeclass_instances. *)
+Global Hint Mode Equiv ! : typeclass_instances. *)
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
 Infix "≡@{ A }" := (@equiv A _)
@@ -251,7 +251,7 @@ with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
 reverse. *)
 Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
-Hint Mode LeibnizEquiv ! - : typeclass_instances.
+Global Hint Mode LeibnizEquiv ! - : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
@@ -283,8 +283,8 @@ Instance: Params (@equiv) 2 := {}.
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3 := {}.
-Hint Extern 0 (_ ≡ _) => reflexivity : core.
-Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
+Global Hint Extern 0 (_ ≡ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 
 
 (** * Type classes *)
@@ -292,7 +292,7 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 (** This type class by (Spitters/van der Weegen, 2011) collects decidable
 propositions. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
-Hint Mode Decision ! : typeclass_instances.
+Global Hint Mode Decision ! : typeclass_instances.
 Arguments decide _ {_} : simpl never, assert.
 
 (** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
@@ -311,14 +311,14 @@ an explicit class instead of a notation for two reasons:
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
   decide_rel x y :> Decision (R x y).
-Hint Mode RelDecision ! ! ! : typeclass_instances.
+Global Hint Mode RelDecision ! ! ! : typeclass_instances.
 Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
 Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
-Hint Mode Inhabited ! : typeclass_instances.
+Global Hint Mode Inhabited ! : typeclass_instances.
 Arguments populate {_} _ : assert.
 
 (** ** Proof irrelevant types *)
@@ -326,7 +326,7 @@ Arguments populate {_} _ : assert.
 elements of the type are equal. We use this notion only used for propositions,
 but by universe polymorphism we can generalize it. *)
 Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
-Hint Mode ProofIrrel ! : typeclass_instances.
+Global Hint Mode ProofIrrel ! : typeclass_instances.
 
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
@@ -462,8 +462,8 @@ Notation "(↔)" := iff (only parsing) : stdpp_scope.
 Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
 Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
 
-Hint Extern 0 (_ ↔ _) => reflexivity : core.
-Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
+Global Hint Extern 0 (_ ↔ _) => reflexivity : core.
+Global Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
 
 Lemma or_l P Q : ¬Q → P ∨ Q ↔ P.
 Proof. tauto. Qed.
@@ -595,9 +595,9 @@ Notation zip := (zip_with pair).
 (** ** Booleans *)
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
-Hint Unfold Is_true : core.
-Hint Immediate Is_true_eq_left : core.
-Hint Resolve orb_prop_intro andb_prop_intro : core.
+Global Hint Unfold Is_true : core.
+Global Hint Immediate Is_true_eq_left : core.
+Global Hint Resolve orb_prop_intro andb_prop_intro : core.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
 Infix "&&*" := (zip_with (&&)) (at level 40).
@@ -813,13 +813,13 @@ relations on sets: the empty set [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
-Hint Mode Empty ! : typeclass_instances.
+Global Hint Mode Empty ! : typeclass_instances.
 Notation "∅" := empty (format "∅") : stdpp_scope.
 
 Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
-Hint Mode Union ! : typeclass_instances.
+Global Hint Mode Union ! : typeclass_instances.
 Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
@@ -833,7 +833,7 @@ Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
 Class DisjUnion A := disj_union: A → A → A.
-Hint Mode DisjUnion ! : typeclass_instances.
+Global Hint Mode DisjUnion ! : typeclass_instances.
 Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
@@ -841,7 +841,7 @@ Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
 Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
-Hint Mode Intersection ! : typeclass_instances.
+Global Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
@@ -849,7 +849,7 @@ Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
 Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
-Hint Mode Difference ! : typeclass_instances.
+Global Hint Mode Difference ! : typeclass_instances.
 Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
@@ -859,7 +859,7 @@ Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 
 Class Singleton A B := singleton: A → B.
-Hint Mode Singleton - ! : typeclass_instances.
+Global Hint Mode Singleton - ! : typeclass_instances.
 Instance: Params (@singleton) 3 := {}.
 Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
@@ -871,7 +871,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z))
   (at level 1, y at next level, z at next level) : stdpp_scope.
 
 Class SubsetEq A := subseteq: relation A.
-Hint Mode SubsetEq ! : typeclass_instances.
+Global Hint Mode SubsetEq ! : typeclass_instances.
 Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
@@ -888,8 +888,8 @@ Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
 Infix "⊆*" := (Forall2 (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : stdpp_scope.
 
-Hint Extern 0 (_ ⊆ _) => reflexivity : core.
-Hint Extern 0 (_ ⊆* _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊆ _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊆* _) => reflexivity : core.
 
 Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope.
@@ -919,10 +919,10 @@ Fixpoint list_to_set_disj `{Singleton A C, Empty C, DisjUnion C} (l : list A) :
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
 Class Lexico A := lexico: relation A.
-Hint Mode Lexico ! : typeclass_instances.
+Global Hint Mode Lexico ! : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
-Hint Mode ElemOf - ! : typeclass_instances.
+Global Hint Mode ElemOf - ! : typeclass_instances.
 Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
@@ -940,7 +940,7 @@ Notation "x ∉@{ B } X" := (¬x ∈@{B} X) (at level 80, only parsing) : stdpp_
 Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
- Hint Mode Disjoint ! : typeclass_instances.
+Global Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
@@ -953,14 +953,14 @@ Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope.
 Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
 Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
 
-Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
-Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
+Global Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
+Global Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
-Hint Mode Filter - ! : typeclass_instances.
+Global Hint Mode Filter - ! : typeclass_instances.
 
 Class UpClose A B := up_close : A → B.
-Hint Mode UpClose - ! : typeclass_instances.
+Global Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
@@ -1018,7 +1018,7 @@ Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
-Hint Mode Lookup - - ! : typeclass_instances.
+Global Hint Mode Lookup - - ! : typeclass_instances.
 Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
@@ -1029,7 +1029,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The function [lookup_total] should be the total over-approximation
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
-Hint Mode LookupTotal - - ! : typeclass_instances.
+Global Hint Mode LookupTotal - - ! : typeclass_instances.
 Instance: Params (@lookup_total) 4 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
 Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
@@ -1039,14 +1039,14 @@ Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
-Hint Mode SingletonM - - ! : typeclass_instances.
+Global Hint Mode SingletonM - - ! : typeclass_instances.
 Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
-Hint Mode Insert - - ! : typeclass_instances.
+Global Hint Mode Insert - - ! : typeclass_instances.
 Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
@@ -1056,14 +1056,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
-Hint Mode Delete - ! : typeclass_instances.
+Global Hint Mode Delete - ! : typeclass_instances.
 Instance: Params (@delete) 4 := {}.
 Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
-Hint Mode Alter - - ! : typeclass_instances.
+Global Hint Mode Alter - - ! : typeclass_instances.
 Instance: Params (@alter) 5 := {}.
 Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1073,14 +1073,14 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
-Hint Mode PartialAlter - - ! : typeclass_instances.
+Global Hint Mode PartialAlter - - ! : typeclass_instances.
 Instance: Params (@partial_alter) 4 := {}.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 set of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
-Hint Mode Dom ! ! : typeclass_instances.
+Global Hint Mode Dom ! ! : typeclass_instances.
 Instance: Params (@dom) 3 := {}.
 Arguments dom : clear implicits.
 Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
@@ -1089,7 +1089,7 @@ Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
-Hint Mode Merge ! : typeclass_instances.
+Global Hint Mode Merge ! : typeclass_instances.
 Instance: Params (@merge) 4 := {}.
 Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1098,20 +1098,20 @@ and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
-Hint Mode UnionWith - ! : typeclass_instances.
+Global Hint Mode UnionWith - ! : typeclass_instances.
 Instance: Params (@union_with) 3 := {}.
 Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
-Hint Mode IntersectionWith - ! : typeclass_instances.
+Global Hint Mode IntersectionWith - ! : typeclass_instances.
 Instance: Params (@intersection_with) 3 := {}.
 Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
-Hint Mode DifferenceWith - ! : typeclass_instances.
+Global Hint Mode DifferenceWith - ! : typeclass_instances.
 Instance: Params (@difference_with) 3 := {}.
 Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1123,7 +1123,7 @@ Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 (** SqSubsetEq registers the "canonical" partial order for a type, and is used
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
-Hint Mode SqSubsetEq ! : typeclass_instances.
+Global Hint Mode SqSubsetEq ! : typeclass_instances.
 Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
@@ -1135,10 +1135,10 @@ Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
 
-Hint Extern 0 (_ ⊑ _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
-Hint Mode Meet ! : typeclass_instances.
+Global Hint Mode Meet ! : typeclass_instances.
 Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
@@ -1146,7 +1146,7 @@ Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
 Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
-Hint Mode Join ! : typeclass_instances.
+Global Hint Mode Join ! : typeclass_instances.
 Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
@@ -1154,11 +1154,11 @@ Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
 Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
 
 Class Top A := top : A.
-Hint Mode Top ! : typeclass_instances.
+Global Hint Mode Top ! : typeclass_instances.
 Notation "⊤" := top (format "⊤") : stdpp_scope.
 
 Class Bottom A := bottom : A.
-Hint Mode Bottom ! : typeclass_instances.
+Global Hint Mode Bottom ! : typeclass_instances.
 Notation "⊥" := bottom (format "⊥") : stdpp_scope.
 
 
@@ -1195,7 +1195,7 @@ Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
-Hint Mode Elements - ! : typeclass_instances.
+Global Hint Mode Elements - ! : typeclass_instances.
 Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
@@ -1231,7 +1231,7 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   NoDup_elements (X : C) : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
-Hint Mode Size ! : typeclass_instances.
+Global Hint Mode Size ! : typeclass_instances.
 Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2 := {}.
 
@@ -1272,7 +1272,7 @@ aforementioned [fresh] function on finite sets that respects set equality.
 Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
-Hint Mode Fresh - ! : typeclass_instances.
+Global Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
 Arguments fresh : simpl never.
 
@@ -1285,6 +1285,6 @@ Arguments infinite_fresh : simpl never.
 
 (** * Miscellaneous *)
 Class Half A := half: A → A.
-Hint Mode Half ! : typeclass_instances.
+Global Hint Mode Half ! : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
diff --git a/theories/coPset.v b/theories/coPset.v
index 1a46079ba5c5c08eb2a072d46bd00eb2ac0182a8..cdf7851ff8169f20bf889755ece50b88f559e8c6 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -45,7 +45,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
 Arguments coPNode' : simpl never.
 Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
 Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
-Hint Resolve coPNode_wf : core.
+Global Hint Resolve coPNode_wf : core.
 
 Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   match t, p with
@@ -184,7 +184,7 @@ Qed.
 
 (** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
 Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
-Hint Resolve coPset_top_subseteq : core.
+Global Hint Resolve coPset_top_subseteq : core.
 
 Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
diff --git a/theories/countable.v b/theories/countable.v
index 2c07d66bcb93bc1ad91a0e96b9d9debb6be95b87..aed78406eb4517dac725dae247b888c6b964f861 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -8,7 +8,7 @@ Class Countable A `{EqDecision A} := {
   decode : positive → option A;
   decode_encode x : decode (encode x) = Some x
 }.
-Hint Mode Countable ! - : typeclass_instances.
+Global Hint Mode Countable ! - : typeclass_instances.
 Arguments encode : simpl never.
 Arguments decode : simpl never.
 
diff --git a/theories/decidable.v b/theories/decidable.v
index 73d175990e8f7c3e821d62cdb5375dec6a021f2a..df16a2edfb23ac92e37e3d40352e076fd869fdbd 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -115,7 +115,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
-Hint Resolve bool_decide_pack : core.
+Global Hint Resolve bool_decide_pack : core.
 
 Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
 Proof. case_bool_decide; intuition discriminate. Qed.
@@ -224,4 +224,4 @@ Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
 (** We do not declare this as an actual instance since Coq can unify [flip ?R]
 with any relation. Coq's standard library is carrying out the same approach for
 the [Reflexive], [Transitive], etc, instance of [flip]. *)
-Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
+Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b86876679f96b59dc1d1cb279cc0066639776f9b..a5aa829ce4f04384ab01e23e7db4d3871b24f51c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -27,8 +27,8 @@ which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
 
 Class FinMapToList K A M := map_to_list: M → list (K * A).
-Hint Mode FinMapToList ! - - : typeclass_instances.
-Hint Mode FinMapToList - - ! : typeclass_instances.
+Global Hint Mode FinMapToList ! - - : typeclass_instances.
+Global Hint Mode FinMapToList - - ! : typeclass_instances.
 
 Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
@@ -99,7 +99,7 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
 Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
   map_relation (λ _ _, False) (λ _, True) (λ _, True).
 Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
+Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
 Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
 Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
@@ -2296,30 +2296,30 @@ Ltac solve_map_disjoint :=
 
 (** We declare these hints using [Hint Extern] instead of [Hint Resolve] as
 [eauto] works badly with hints parametrized by type class constraints. *)
-Hint Extern 1 (_ ##ₘ _) => done : map_disjoint.
-Hint Extern 2 (∅ ##ₘ _) => apply map_disjoint_empty_l : map_disjoint.
-Hint Extern 2 (_ ##ₘ ∅) => apply map_disjoint_empty_r : map_disjoint.
-Hint Extern 2 ({[ _ := _ ]} ##ₘ _) =>
+Global Hint Extern 1 (_ ##ₘ _) => done : map_disjoint.
+Global Hint Extern 2 (∅ ##ₘ _) => apply map_disjoint_empty_l : map_disjoint.
+Global Hint Extern 2 (_ ##ₘ ∅) => apply map_disjoint_empty_r : map_disjoint.
+Global Hint Extern 2 ({[ _ := _ ]} ##ₘ _) =>
   apply map_disjoint_singleton_l_2 : map_disjoint.
-Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
+Global Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
   apply map_disjoint_singleton_r_2 : map_disjoint.
-Hint Extern 2 (_ ∪ _ ##ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
-Hint Extern 2 (_ ##ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
-Hint Extern 2 ({[_:= _]} ##ₘ _) => apply map_disjoint_singleton_l : map_disjoint.
-Hint Extern 2 (_ ##ₘ {[_:= _]}) => apply map_disjoint_singleton_r : map_disjoint.
-Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
-Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
-Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.
-Hint Extern 2 (_ ##ₘ delete _ _) => apply map_disjoint_delete_r : map_disjoint.
-Hint Extern 2 (list_to_map _ ##ₘ _) =>
+Global Hint Extern 2 (_ ∪ _ ##ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
+Global Hint Extern 2 (_ ##ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
+Global Hint Extern 2 ({[_:= _]} ##ₘ _) => apply map_disjoint_singleton_l : map_disjoint.
+Global Hint Extern 2 (_ ##ₘ {[_:= _]}) => apply map_disjoint_singleton_r : map_disjoint.
+Global Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
+Global Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
+Global Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.
+Global Hint Extern 2 (_ ##ₘ delete _ _) => apply map_disjoint_delete_r : map_disjoint.
+Global Hint Extern 2 (list_to_map _ ##ₘ _) =>
   apply map_disjoint_list_to_map_zip_l_2 : mem_disjoint.
-Hint Extern 2 (_ ##ₘ list_to_map _) =>
+Global Hint Extern 2 (_ ##ₘ list_to_map _) =>
   apply map_disjoint_list_to_map_zip_r_2 : mem_disjoint.
-Hint Extern 2 (⋃ _ ##ₘ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
-Hint Extern 2 (_ ##ₘ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
-Hint Extern 2 (foldr delete _ _ ##ₘ _) =>
+Global Hint Extern 2 (⋃ _ ##ₘ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
+Global Hint Extern 2 (_ ##ₘ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
+Global Hint Extern 2 (foldr delete _ _ ##ₘ _) =>
   apply map_disjoint_foldr_delete_l : map_disjoint.
-Hint Extern 2 (_ ##ₘ foldr delete _ _) =>
+Global Hint Extern 2 (_ ##ₘ foldr delete _ _) =>
   apply map_disjoint_foldr_delete_r : map_disjoint.
 
 (** The tactic [simpl_map by tac] simplifies occurrences of finite map look
@@ -2367,10 +2367,10 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
 Create HintDb simpl_map discriminated.
 Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map map_disjoint.
 
-Hint Extern 80 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
-Hint Extern 81 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_r : simpl_map.
-Hint Extern 80 ({[ _:=_ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
-Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
+Global Hint Extern 80 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
+Global Hint Extern 81 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_r : simpl_map.
+Global Hint Extern 80 ({[ _:=_ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
+Global Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
 
 (** Now we take everything together and also discharge conflicting look ups,
 simplify overlapping look ups, and perform cancellations of equalities
diff --git a/theories/finite.v b/theories/finite.v
index 392075251b342707891cccbe75c07ee89f0001ec..7347e1a010824ddcbfbbac820f7dc3b94c0776ec 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -7,7 +7,7 @@ Class Finite A `{EqDecision A} := {
   NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
 }.
-Hint Mode Finite ! - : typeclass_instances.
+Global Hint Mode Finite ! - : typeclass_instances.
 Arguments enum : clear implicits.
 Arguments enum _ {_ _} : assert.
 Arguments NoDup_enum : clear implicits.
@@ -26,7 +26,7 @@ Next Obligation.
   rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
   destruct (list_find_Some (x =.) xs i y); naive_solver.
 Qed.
-Hint Immediate finite_countable : typeclass_instances.
+Global Hint Immediate finite_countable : typeclass_instances.
 
 Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A :=
   list_find P (enum A) ≫= decode_nat ∘ fst.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 5729b0926aec6a148f985dcbe1c0eb39e34eeeaa..fbff2e5856b1b15852c0c20936e56742f143df5d 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -170,7 +170,7 @@ universally quantified hypotheses [H : ∀ x : A, P x] in two ways:
 Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
   { multiset_unfold : multiplicity x X = n }.
 Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
-Hint Mode MultisetUnfold + + + - + - : typeclass_instances.
+Global Hint Mode MultisetUnfold + + + - + - : typeclass_instances.
 
 Section multiset_unfold.
   Context `{Countable A}.
diff --git a/theories/list.v b/theories/list.v
index 25ee557646d775a5d0ab6a4719c04384a498d44e..25b5e23e96f5d447b89b5c93dda489b7b474361f 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -272,8 +272,8 @@ Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
 Definition prefix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
 Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
 Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
-Hint Extern 0 (_ `prefix_of` _) => reflexivity : core.
-Hint Extern 0 (_ `suffix_of` _) => reflexivity : core.
+Global Hint Extern 0 (_ `prefix_of` _) => reflexivity : core.
+Global Hint Extern 0 (_ `suffix_of` _) => reflexivity : core.
 
 Section prefix_suffix_ops.
   Context `{EqDecision A}.
@@ -302,7 +302,7 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
   | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
 Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
-Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
+Global Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
 
 (** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
 from [l1] while possiblity changing the order. *)
@@ -313,7 +313,7 @@ Inductive submseteq {A} : relation (list A) :=
   | submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
   | submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
 Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 
 (** Removes [x] from the list [l]. The function returns a [Some] when the
 +removal succeeds and [None] when [x] is not in [l]. *)
diff --git a/theories/namespaces.v b/theories/namespaces.v
index b68326b5720a52ee2e988daf40a1c01c231acbab..dccbca7c650107064cbf94f45137dd2a75add8d9 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -79,30 +79,30 @@ Create HintDb ndisj discriminated.
 (** If-and-only-if rules. Well, not quite, but for the fragment we are
 considering they are. *)
 Local Definition coPset_subseteq_difference_r := subseteq_difference_r (C:=coPset).
-Hint Resolve coPset_subseteq_difference_r : ndisj.
+Global Hint Resolve coPset_subseteq_difference_r : ndisj.
 Local Definition coPset_empty_subseteq := empty_subseteq (C:=coPset).
-Hint Resolve coPset_empty_subseteq : ndisj.
+Global Hint Resolve coPset_empty_subseteq : ndisj.
 Local Definition coPset_union_least := union_least (C:=coPset).
-Hint Resolve coPset_union_least : ndisj.
+Global Hint Resolve coPset_union_least : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Local Definition coPset_subseteq_difference_l := subseteq_difference_l (C:=coPset).
-Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
-Hint Resolve nclose_subseteq' | 100 : ndisj.
+Global Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
+Global Hint Resolve nclose_subseteq' | 100 : ndisj.
 
 (** Rules for goals of the form [_ ## _] *)
 (** The base rule that we want to ultimately get down to. *)
-Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
+Global Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress.
 Tests show trying [disjoint_difference_l1] first gives better performance. *)
 Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
-Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
+Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
 Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
-Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
-Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
+Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
+Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
   | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
   end;
   solve [eauto 12 with ndisj].
-Hint Extern 1000 => solve_ndisj : solve_ndisj.
+Global Hint Extern 1000 => solve_ndisj : solve_ndisj.
diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index 2ae1bfa48e8c18c9fe15f5da5b19f49d9e110ff8..218a21a903c962d48fc61c7eb0f5caff14f108b4 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -38,13 +38,13 @@ approach based on reflection would be better, but for small inputs, the overhead
 of reification will probably not be worth it. *)
 
 Class NatCancel (m n m' n' : nat) := nat_cancel : m' + n = m + n'.
-Hint Mode NatCancel ! ! - - : typeclass_instances.
+Global Hint Mode NatCancel ! ! - - : typeclass_instances.
 
 Module nat_cancel.
   Class NatCancelL (m n m' n' : nat) := nat_cancel_l : m' + n = m + n'.
-  Hint Mode NatCancelL ! ! - - : typeclass_instances.
+  Global Hint Mode NatCancelL ! ! - - : typeclass_instances.
   Class NatCancelR (m n m' n' : nat) := nat_cancel_r : NatCancelL m n m' n'.
-  Hint Mode NatCancelR ! ! - - : typeclass_instances.
+  Global Hint Mode NatCancelR ! ! - - : typeclass_instances.
   Existing Instance nat_cancel_r | 100.
 
   (** The implementation of the canceler is highly non-deterministic, but since
diff --git a/theories/numbers.v b/theories/numbers.v
index ed42de032fef46f7db6652e78b06303c6676a057..e18ff11a6af322644f3f9057cd8cc2b4e2622f7d 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -89,7 +89,7 @@ Instance: PartialOrder divide.
 Proof.
   repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
 Qed.
-Hint Extern 0 (_ | _) => reflexivity : core.
+Global Hint Extern 0 (_ | _) => reflexivity : core.
 Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
 Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
 
@@ -314,7 +314,7 @@ Qed.
 Instance N_le_total: Total (≤)%N.
 Proof. repeat intro; lia. Qed.
 
-Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
+Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
 
 (** * Notations and properties of [Z] *)
 Local Open Scope Z_scope.
@@ -410,12 +410,12 @@ Proof. by destruct x. Qed.
 Lemma Z_mod_pos x y : 0 < y → 0 ≤ x `mod` y.
 Proof. apply Z.mod_pos_bound. Qed.
 
-Hint Resolve Z.lt_le_incl : zpos.
-Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
-Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
-Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
-Hint Resolve Z_mod_pos Z.div_pos : zpos.
-Hint Extern 1000 => lia : zpos.
+Global Hint Resolve Z.lt_le_incl : zpos.
+Global Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
+Global Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
+Global Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
+Global Hint Resolve Z_mod_pos Z.div_pos : zpos.
+Global Hint Extern 1000 => lia : zpos.
 
 Lemma Z_to_nat_nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
 Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
@@ -509,7 +509,7 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
 Notation "(≤)" := Qcle (only parsing) : Qc_scope.
 Notation "(<)" := Qclt (only parsing) : Qc_scope.
 
-Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core.
+Global Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core.
 Arguments Qred : simpl never.
 
 Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
@@ -740,7 +740,7 @@ Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope
 Notation "(≤)" := Qp_le (only parsing) : Qp_scope.
 Notation "(<)" := Qp_lt (only parsing) : Qp_scope.
 
-Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
+Global Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
 
 Lemma Qp_to_Qc_inj_le p q : p ≤ q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
 Proof. by destruct p, q. Qed.
diff --git a/theories/option.v b/theories/option.v
index 545c884b45e2d64eec4e511ded34c51a00e48b3c..cd88494a1fc46a18947289b54f97d308be8ddc1c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -46,10 +46,10 @@ Proof. unfold is_Some. destruct mx; naive_solver. Qed.
 
 Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx.
 Proof. intros; red; subst; eauto. Qed.
-Hint Resolve mk_is_Some : core.
+Global Hint Resolve mk_is_Some : core.
 Lemma is_Some_None {A} : ¬is_Some (@None A).
 Proof. by destruct 1. Qed.
-Hint Resolve is_Some_None : core.
+Global Hint Resolve is_Some_None : core.
 
 Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx.
 Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
diff --git a/theories/pretty.v b/theories/pretty.v
index e1a28d941d372b6c0a87453396aa31f4ad6e4de8..004142b0e0540257ff33bcda4958c64ba6e138fa 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -4,7 +4,7 @@ From Coq Require Import Ascii.
 From stdpp Require Import options.
 
 Class Pretty A := pretty : A → string.
-Hint Mode Pretty ! : typeclass_instances.
+Global Hint Mode Pretty ! : typeclass_instances.
 
 Definition pretty_N_char (x : N) : ascii :=
   match x with
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index e1d3ebd9b029fa8dc4828dfbcbe75f03b4294c06..b972df7448d670c57da014577ac78dd19f8b1436 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -2,7 +2,7 @@
 From stdpp Require Export base.
 From stdpp Require Import options.
 
-Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
+Global Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
 Instance True_pi: ProofIrrel True.
 Proof. intros [] []; reflexivity. Qed.
diff --git a/theories/relations.v b/theories/relations.v
index 5668bcc4c07501e969fbc267a05fca00f3cc9eb9..81737ed495012993dd8bd1764db78ef5637ed3a1 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -75,7 +75,7 @@ Definition confluent {A} (R : relation A) :=
 Definition locally_confluent {A} (R : relation A) :=
   ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z.
 
-Hint Unfold nf red : core.
+Global Hint Unfold nf red : core.
 
 (** * General theorems *)
 Section closure.
diff --git a/theories/sets.v b/theories/sets.v
index b0522842a41ba2412de3fba4e0df0defab50e871..e16de487227d8b0a4d9a4274784cfd31f9f89350 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -96,14 +96,14 @@ rewriting to ensure that we traverse each term at most once and to be able to
 deal with occurences of the set operations under binders. *)
 Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
 Arguments set_unfold _ _ {_} : assert.
-Hint Mode SetUnfold + - : typeclass_instances.
+Global Hint Mode SetUnfold + - : typeclass_instances.
 
 (** The class [SetUnfoldElemOf] is a more specialized version of [SetUnfold]
 for propositions of the shape [x ∈ X] to improve performance. *)
 Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
   { set_unfold_elem_of : x ∈ X ↔ Q }.
 Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
-Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
+Global Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
 
 Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
   SetUnfoldElemOf x X (x ∈ X) | 1000.
@@ -113,7 +113,7 @@ Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
 Proof. by destruct 1; constructor. Qed.
 
 Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
-Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
+Global Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
 
 Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
 Definition set_unfold_1 `{SetUnfold P Q} : P → Q := proj1 (set_unfold P Q).
@@ -142,19 +142,19 @@ Proof. constructor. naive_solver. Qed.
 
 (* Avoid too eager application of the above instances (and thus too eager
 unfolding of type class transparent definitions). *)
-Hint Extern 0 (SetUnfold (_ → _) _) =>
+Global Hint Extern 0 (SetUnfold (_ → _) _) =>
   class_apply set_unfold_impl : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ∧ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ∧ _) _) =>
   class_apply set_unfold_and : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ∨ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ∨ _) _) =>
   class_apply set_unfold_or : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ↔ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ↔ _) _) =>
   class_apply set_unfold_iff : typeclass_instances.
-Hint Extern 0 (SetUnfold (¬ _) _) =>
+Global Hint Extern 0 (SetUnfold (¬ _) _) =>
   class_apply set_unfold_not : typeclass_instances.
-Hint Extern 1 (SetUnfold (∀ _, _) _) =>
+Global Hint Extern 1 (SetUnfold (∀ _, _) _) =>
   class_apply set_unfold_forall : typeclass_instances.
-Hint Extern 0 (SetUnfold (∃ _, _) _) =>
+Global Hint Extern 0 (SetUnfold (∃ _, _) _) =>
   class_apply set_unfold_exist : typeclass_instances.
 
 Section set_unfold_simple.
@@ -347,9 +347,9 @@ Tactic Notation "set_solver" := set_solver by idtac.
 Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
 Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
 
-Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
-Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
-Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
 
 
 (** * Sets with [∪], [∅] and [{[_]}] *)
diff --git a/theories/tactics.v b/theories/tactics.v
index 781b59a9cb125cbf6dff02c3e117146748e53db9..47401180e0b4f04b856578fab58a43bdd03ed899 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -21,11 +21,11 @@ Ltac f_equal :=
 (** We declare hint databases [f_equal], [congruence] and [lia] and containing
 solely the tactic corresponding to its name. These hint database are useful in
 to be combined in combination with other hint database. *)
-Hint Extern 998 (_ = _) => f_equal : f_equal.
-Hint Extern 999 => congruence : congruence.
-Hint Extern 1000 => lia : lia.
-Hint Extern 1000 => omega : omega.
-Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
+Global Hint Extern 998 (_ = _) => f_equal : f_equal.
+Global Hint Extern 999 => congruence : congruence.
+Global Hint Extern 1000 => lia : lia.
+Global Hint Extern 1000 => omega : omega.
+Global Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
 be very bad, so use with care! *)
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 6582ccc86cf93e5bf31eeea6d0cbf8d07d8f37ca..55beb892060fbd9a090ba651ee09ed90dd7104ad 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -189,7 +189,7 @@ Qed.
 
 (* Teach typeclass resolution how to make progress on these binders *)
 Typeclasses Opaque tforall texist.
-Hint Extern 1 (tforall _) =>
+Global Hint Extern 1 (tforall _) =>
   progress cbn [tforall tele_fold tele_bind tele_app] : typeclass_instances.
-Hint Extern 1 (texist _) =>
+Global Hint Extern 1 (texist _) =>
   progress cbn [texist tele_fold tele_bind tele_app] : typeclass_instances.