From 3081c4419248ef25e3359275d6266125159398b4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jan 2021 13:26:54 +0100
Subject: [PATCH] also adjust Hint

---
 theories/gmultiset.v | 2 +-
 theories/list.v      | 2 +-
 theories/relations.v | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 371db3e2..3d164a8e 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 21923526..d8faeaf0 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 81737ed4..46b8d580 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.
-- 
GitLab