diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 371db3e28ccc760003defa28270c846e3d5ab7f6..3d164a8e8394e9075b4409ad8ce0a2a9e0e643bb 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -470,7 +470,7 @@ Section more_lemmas.
 
   Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
   Proof. apply strict_include. Qed.
-  Hint Resolve gmultiset_subset_subseteq : core.
+  Local Hint Resolve gmultiset_subset_subseteq : core.
 
   Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
   Proof. multiset_solver. Qed.
diff --git a/theories/list.v b/theories/list.v
index 21923526acd9688bcd69e2f939f5c58d5ae63227..d8faeaf085f458044b8cd1454d23d20c1cf7651c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3113,7 +3113,7 @@ End Forall2_proper.
 
 Section Forall3.
   Context {A B C} (P : A → B → C → Prop).
-  Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
+  Local Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
 
   Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
     Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
diff --git a/theories/relations.v b/theories/relations.v
index 81737ed495012993dd8bd1764db78ef5637ed3a1..46b8d580bdc4f7941afe92a8697e7e7ab9dcb1bc 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -81,7 +81,7 @@ Global Hint Unfold nf red : core.
 Section closure.
   Context `{R : relation A}.
 
-  Hint Constructors rtc nsteps bsteps tc : core.
+  Local Hint Constructors rtc nsteps bsteps tc : core.
 
   Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z.
   Proof. induction 1; eauto. Qed.
@@ -271,7 +271,7 @@ End more_closure.
 Section properties.
   Context `{R : relation A}.
 
-  Hint Constructors rtc nsteps bsteps tc : core.
+  Local Hint Constructors rtc nsteps bsteps tc : core.
 
   Lemma nf_wn x : nf R x → wn R x.
   Proof. intros. exists x; eauto. Qed.