diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8f4294bd0b203d18277b441e7a4868e9aa76de37..8750ba4740673b810861559bb54c841a478e7e1d 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -24,7 +24,7 @@ Ltac solve_proto_contractive :=
 (** * Normalization of protocols *)
 Class ActionDualIf (d : bool) (a1 a2 : action) :=
   dual_action_if : a2 = if d then action_dual a1 else a1.
-Hint Mode ActionDualIf ! ! - : typeclass_instances.
+Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
 
 Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
 Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
@@ -35,7 +35,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
   proto_normalize :
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ curry iProto_dual_if) END%proto pas ⊑ q.
-Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
+Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
 Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
@@ -45,7 +45,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
     (pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
-Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
+Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
 Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
 
 Section classes.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 2c91fda189283b5687a90cab2ce281e5211f1d47..111c9ee97a6bf63ef551cadaa1e14201dc3fb5f7 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -191,7 +191,7 @@ Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
 Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
     (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
   msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
-Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
+Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
 
 (** * Operations *)
 Program Definition iMsg_map {Σ V}
@@ -1295,5 +1295,5 @@ End proto.
 
 Typeclasses Opaque iProto_ctx iProto_own.
 
-Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
+Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 1a79e7dc4da2a8896c31dd7a855f065001b538d1..d04230c943a69b26e65b36ed7daef39eaa14be00 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -78,7 +78,7 @@ Notation "(.<++> T )" := (λ S, lty_app S T) (only parsing) : lty_scope.
 Class LtyMsgTele {Σ} {kt : ktele Σ} (M : lmsg Σ)
     (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :=
   lty_msg_tele : M ≡ (∃.. x, TY ktele_app A x; ktele_app S x)%lmsg.
-Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
+Global Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
 
 Section session_types.
   Context {Σ : gFunctors}.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 321edfd013bf869dcebf9c31d5a82b8ed0ef467a..7ee3bfc814521a135f628028dcff86cbf110072b 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -606,5 +606,5 @@ Section subtyping_rules.
 
 End subtyping_rules.
 
-Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
+Global Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply lty_le_refl] : core.