diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 7a6422176b12771890a0de48cfa77fe7fa622b0e..93b47498c79d4bd207f36de801b2205463aac92e 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -47,7 +47,7 @@ Proof. by unlock. Qed.
 
 Class DoSubst (x : binder) (es : expr) (e er : expr) :=
   do_subst : subst' x es e = er.
-Hint Extern 0 (DoSubst _ _ _ _) =>
+Global Hint Extern 0 (DoSubst _ _ _ _) =>
   rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
 
 Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 0887d4d761f24ab0076d2c6737ae015224f32b69..e49c8111b50dbf0488ac59d084c913b0d8e5b706 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -175,7 +175,7 @@ Ltac solve_closed :=
      let e' := W.of_expr e in change (Closed X (W.to_expr e'));
      apply W.is_closed_correct; vm_compute; exact I
   end.
-Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+Global Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
 Ltac solve_into_val :=
   match goal with
@@ -184,7 +184,7 @@ Ltac solve_into_val :=
      apply W.to_val_Some; simpl; unfold W.to_expr;
      ((unlock; exact eq_refl) || (idtac; exact eq_refl))
   end.
-Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
+Global Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
 
 Ltac solve_as_val :=
   match goal with
@@ -192,7 +192,7 @@ Ltac solve_as_val :=
      let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
-Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
+Global Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
@@ -200,7 +200,7 @@ Ltac solve_atomic :=
      let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
      apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
+Global Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
 
 Global Instance skip_atomic : Atomic WeaklyAtomic Skip.
 Proof.
diff --git a/theories/typing/base.v b/theories/typing/base.v
index f5a8b0029464777523b6172e554b656138633dbb..f5cb2484832362f36f4696b9dacc0510c2c8258b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -20,18 +20,18 @@ Ltac solve_typing :=
   (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
   (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
 
-Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
+Global Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
+Global Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
   : lrust_typing.
 
-Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
+Global Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
   (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
-Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
+Global Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
   (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
 
-Hint Resolve <- elem_of_app : lrust_typing.
+Global Hint Resolve <- elem_of_app : lrust_typing.
 
 (* done is there to handle equalities with constants *)
-Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 2df1328be476ad369a69b62210b28b6fe43cbc22..baf447ff044341e108f67dafeaa720168818ca75 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -212,7 +212,7 @@ Section borrow.
   Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
 End borrow.
 
-Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
+Global Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
                | 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 118434980ae6ff80445a78658c9d73f8f1a92001..b76fdf65bb167958b2508255624e90990ef56456 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -116,4 +116,4 @@ Section cont_context.
   Qed.
 End cont_context.
 
-Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
+Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 3efd7862044d39e8d2c981f09251c622ce438b96..76c9e197d47303448418d6d964f32d021fbbd590 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -141,11 +141,11 @@ Section subtyping.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
 End subtyping.
 
-Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
+Global Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
 
 (* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
    not been tried before, so we give them a high cost *)
-Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fac54aac4b3fc1fd9446cfd32804359749df1680..534f80e5a18ded87902d6c4b550e6350519b0ea2 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -444,4 +444,4 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve fn_subtype : lrust_typing.
+Global Hint Resolve fn_subtype : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 2525bdfc300318fb07ffa9eb407776e19dcacfbf..268f972b10b15638d3382d338203073bab7bc380 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -419,7 +419,7 @@ Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
-Hint Resolve
+Global Hint Resolve
      lctx_lft_incl_refl lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external' lctx_lft_incl_intersect
      lctx_lft_incl_intersect_l lctx_lft_incl_intersect_r
@@ -427,8 +427,8 @@ Hint Resolve
      elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
   : lrust_typing.
 
-Hint Extern 10 (lctx_lft_eq _ _ _ _) => split : lrust_typing.
+Global Hint Extern 10 (lctx_lft_eq _ _ _ _) => split : lrust_typing.
 
-Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
+Global Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
 
-Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
+Global Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index ae86479bff86846a560cd4278f40e03cd13b5fd8..b0e90f84803d125b49ac59db48938104512da1b1 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -253,4 +253,4 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve cell_mono' cell_proper' : lrust_typing.
+Global Hint Resolve cell_mono' cell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index f50312d3ffde3f4456b0004573672a436ffe60e0..ccbcbb4763ae134aa1369affa8ac427e9f15cf4e 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -113,4 +113,4 @@ Section ref.
   Proof. intros. by eapply ref_proper. Qed.
 End ref.
 
-Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
+Global Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index b089b73dc9bbba32869667a817ebb4a78d442894..23ad8be5186ddb910e8332a8e9a524c9ba4cd3a1 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -209,4 +209,4 @@ Section refcell.
   Proof. move=>???[|[[]|]]//=. Qed.
 End refcell.
 
-Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
+Global Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 3da42ad70231601cce3089d7a29ebf7058d26902..9a0be7e7babae92dfde488da18aeccf81f3d82a9 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -125,4 +125,4 @@ Section refmut.
   Proof. intros. by eapply refmut_proper. Qed.
 End refmut.
 
-Hint Resolve refmut_mono' refmut_proper' : lrust_typing.
+Global Hint Resolve refmut_mono' refmut_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 889ec4d10df8783ac1b0b0aa3589f7bdf4fbfae3..c462ce0b931bb6e32332dc675d58cb550035c92e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -226,4 +226,4 @@ Section rwlock.
   Qed.
 End rwlock.
 
-Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
+Global Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e33822fca1e791204c7df40d073b37ae07097274..e39ef04481a6a04830f6565e6e1834a88ebbadf2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -137,4 +137,4 @@ Section rwlockreadguard.
   Qed.
 End rwlockreadguard.
 
-Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
+Global Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 0342b547b83b9f522a084f2ae69810ece28a3d39..5b348f3da93c333bce56e7399b9908cf92fe2355 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -143,4 +143,4 @@ Section rwlockwriteguard.
   Qed.
 End rwlockwriteguard.
 
-Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
+Global Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 3de55448c0fc7a379ae4b7055358be64d82804b0..2d246eb10c26d8399ad790c01092dda41004a68c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -362,8 +362,8 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve own_mono' own_proper' box_mono' box_proper'
+Global Hint Resolve own_mono' own_proper' box_mono' box_proper'
              write_own read_own_copy : lrust_typing.
 (* By setting the priority high, we make sure copying is tried before
    moving. *)
-Hint Resolve read_own_move | 100 : lrust_typing.
+Global Hint Resolve read_own_move | 100 : lrust_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index d1d5b103a0e320b3a0c790753e06fab25f1d3bbc..605039859e9377525c185003e86cf0a5978fca16 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -262,6 +262,6 @@ Section typing.
 End typing.
 
 Arguments product : simpl never.
-Hint Opaque product : lrust_typing lrust_typing_merge.
-Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
+Global Hint Opaque product : lrust_typing lrust_typing_merge.
+Global Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
   : lrust_typing.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3c2ff90b9beffd97008f700926ccb08879251fc2..8e3e8ec207a7a4a99627a3fc33ba488228bfff9b 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -302,11 +302,11 @@ End product_split.
 
 (* We do not want unification to try to unify the definition of these
    types with anything in order to try splitting or merging. *)
-Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Global Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
 
 (* We make sure that splitting is tried before borrowing, so that not
    the entire product is borrowed when only a part is needed. *)
-Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
+Global Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
     | 5 : lrust_typing.
 
 (* Merging is also tried after everything, except
@@ -319,6 +319,6 @@ Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extra
    solve_typing get slow because of that. See:
      https://coq.inria.fr/bugs/show_bug.cgi?id=5304
 *)
-Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
+Global Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
     | 40 : lrust_typing_merge.
-Hint Unfold extract_tyl : lrust_typing.
+Global Hint Unfold extract_tyl : lrust_typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 18b0c8176040df21fbcd04248a3bbae97267530b..471a6775a4693adad84b84b3714d70b2eafadc59 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -98,4 +98,4 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.
+Global Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 55e1a493cc528db93a167ae4e2fe4cf5b4983ba0..ebf0d432f9ce774c575d954be6b243c1c10e39ef 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -240,5 +240,5 @@ End sum.
 Notation "Σ[ ty1 ; .. ; tyn ]" :=
   (sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
 
-Hint Opaque sum : lrust_typing lrust_typing_merge.
-Hint Resolve sum_mono' sum_proper' : lrust_typing.
+Global Hint Opaque sum : lrust_typing lrust_typing_merge.
+Global Hint Resolve sum_mono' sum_proper' : lrust_typing.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index aa1c630d5b88c77bf01b82a2433b64df31ae656f..384c1089c36134cb78835e65898d16e1b3c8d357 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -757,6 +757,6 @@ Section type_util.
 
 End type_util.
 
-Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
-Hint Resolve subtype_refl eqtype_refl : lrust_typing.
-Hint Opaque subtype eqtype : lrust_typing.
+Global Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
+Global Hint Resolve subtype_refl eqtype_refl : lrust_typing.
+Global Hint Opaque subtype eqtype : lrust_typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index ce685e63d5fc967fc70674309db5b0d980aeb839..d77939a3ae8d417c1775a9d7ad5a2b7704f3fb3e 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -319,17 +319,17 @@ Section type_context.
   Qed.
 End type_context.
 
-Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
-Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
-Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
-Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
+Global Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
+Global Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
              tctx_extract_ctx_nil tctx_extract_ctx_hasty
              tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing.
-Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
+Global Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
             tctx_incl : lrust_typing.
 
 (* In general, we want reborrowing to be tried before subtyping, so
    that we get the extraction. However, in the case the types match
    exactly, we want to NOT use reborrowing. Therefore, we add
    [tctx_extract_hasty_here_eq] as a hint with a very low cost. *)
-Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index b0a513f9b86dd412ea806c5969f3ebae2e8c215b..9c4f033e24026c6dac4ea1059e4c2dcb604a2d59 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -294,4 +294,4 @@ Section case.
   Qed.
 End case.
 
-Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.
+Global Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 214c359f1aaae06ac98b3463810d04a8ae4a4a0f..bddc962240879d27390f02e5fe4913ab9478128a 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -132,7 +132,7 @@ Section uninit.
   Proof. rewrite -uninit_uninit0_eqtype=>->//. Qed.
 End uninit.
 
-Hint Resolve uninit_product_eqtype_cons_l uninit_product_eqtype_cons_r
+Global Hint Resolve uninit_product_eqtype_cons_l uninit_product_eqtype_cons_r
              uninit_product_subtype_cons_l uninit_product_subtype_cons_r
              uninit_unit_eqtype uninit_unit_eqtype'
              uninit_unit_subtype uninit_unit_subtype' : lrust_typing.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0c747e2984f26649c985878a69f574a242674d81..badff4b257748ac69467c118e3499c898fd7b556 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -173,5 +173,5 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
-Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.
+Global Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.