From 247db01f6784425758efa4c4d2769b6b465ba924 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Thu, 3 Dec 2020 09:21:59 -0600
Subject: [PATCH] Add explicit Local to non-Global hints

---
 iris/algebra/dra.v                      |  4 ++--
 iris/algebra/sts.v                      | 22 +++++++++++-----------
 iris/base_logic/upred.v                 |  2 +-
 iris/bi/derived_laws.v                  | 14 +++++++-------
 iris/bi/derived_laws_later.v            |  6 +++---
 iris/bi/internal_eq.v                   |  8 ++++----
 iris/bi/monpred.v                       |  2 +-
 iris/bi/plainly.v                       |  6 +++---
 iris/program_logic/ectx_lifting.v       |  6 +++---
 iris/program_logic/language.v           |  4 ++--
 iris/program_logic/lifting.v            |  2 +-
 iris/program_logic/ownp.v               |  6 +++---
 iris/program_logic/total_ectx_lifting.v |  2 +-
 iris/program_logic/total_lifting.v      |  2 +-
 iris/proofmode/environments.v           |  2 +-
 15 files changed, 44 insertions(+), 44 deletions(-)

diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index 5d8679358..fa43cb751 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -141,11 +141,11 @@ Proof.
   intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
   apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
-Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
+Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
 
 Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
-Hint Resolve validity_valid_car_valid : core.
+Local Hint Resolve validity_valid_car_valid : core.
 Program Instance validity_pcore : PCore (validity A) := λ x,
   Some (Validity (core (validity_car x)) (✓ x) _).
 Solve Obligations with naive_solver eauto using dra_core_valid.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 65257373f..c35d4c75d 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -54,12 +54,12 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
   S ≫= λ s, up s T.
 
 (** Tactic setup *)
-Hint Resolve Step : core.
-Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (_ ∈ _) => set_solver : sts.
-Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-Hint Extern 50 (_ ## _) => set_solver : sts.
+Local Hint Resolve Step : core.
+Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Local Hint Extern 50 (_ ⊆ _) => set_solver : sts.
+Local Hint Extern 50 (_ ## _) => set_solver : sts.
 
 (** ** Setoids *)
 Instance frame_step_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
@@ -221,11 +221,11 @@ Instance sts_op : Op (car sts) := λ x1 x2,
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2)(* never happens *)
   end.
 
-Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
-Hint Extern 50 (∃ s : state sts, _) => set_solver : sts.
-Hint Extern 50 (_ ∈ _) => set_solver : sts.
-Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-Hint Extern 50 (_ ## _) => set_solver : sts.
+Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
+Local Hint Extern 50 (∃ s : state sts, _) => set_solver : sts.
+Local Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Local Hint Extern 50 (_ ⊆ _) => set_solver : sts.
+Local Hint Extern 50 (_ ## _) => set_solver : sts.
 
 Global Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s).
 Proof. by constructor. Qed.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 2cf522d11..8cfae37ef 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -429,7 +429,7 @@ Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
 Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails : core.
+Local Hint Immediate uPred_in_entails : core.
 
 Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
 Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 8f7c63fd0..8dc90eaff 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -21,7 +21,7 @@ Implicit Types P Q R : PROP.
 Implicit Types Ps : list PROP.
 Implicit Types A : Type.
 
-Hint Extern 100 (NonExpansive _) => solve_proper : core.
+Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
 (* Force implicit argument PROP *)
 Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
@@ -95,9 +95,9 @@ Proof. intros ->; apply exist_intro. Qed.
 Lemma forall_elim' {A} P (Ψ : A → PROP) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
 Proof. move=> HP a. by rewrite HP forall_elim. Qed.
 
-Hint Resolve pure_intro forall_intro : core.
-Hint Resolve or_elim or_intro_l' or_intro_r' : core.
-Hint Resolve and_intro and_elim_l' and_elim_r' : core.
+Local Hint Resolve pure_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
+Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
 
 Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
 Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
@@ -114,7 +114,7 @@ Lemma False_elim P : False ⊢ P.
 Proof. by apply (pure_elim' False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply pure_intro. Qed.
-Hint Immediate False_elim : core.
+Local Hint Immediate False_elim : core.
 
 Lemma entails_eq_True P Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I).
 Proof.
@@ -337,7 +337,7 @@ Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
 
 
 (* BI Stuff *)
-Hint Resolve sep_mono : core.
+Local Hint Resolve sep_mono : core.
 Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'.
 Proof. by intros; apply sep_mono. Qed.
 Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'.
@@ -810,7 +810,7 @@ Section bi_affine.
 End bi_affine.
 
 (* Properties of the persistence modality *)
-Hint Resolve persistently_mono : core.
+Local Hint Resolve persistently_mono : core.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 Global Instance persistently_flip_mono' :
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 3f61a09c4..798d76859 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -17,14 +17,14 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
 Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
-Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
 
 Global Instance later_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
 
 (* Later derived *)
-Hint Resolve later_mono : core.
+Local Hint Resolve later_mono : core.
 Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@bi_later PROP).
 Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 593d7cf7f..837d60c16 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -85,10 +85,10 @@ Global Instance internal_eq_proper (A : ofeT) :
   Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
 
 (* Equality *)
-Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-Hint Resolve internal_eq_refl : core.
-Hint Extern 100 (NonExpansive _) => solve_proper : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+Local Hint Resolve internal_eq_refl : core.
+Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
 Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. intros ->. auto. Qed.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index bc1ca58ae..39f88ff74 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -121,7 +121,7 @@ Implicit Types P Q : monPred.
 
 Inductive monPred_entails (P1 P2 : monPred) : Prop :=
   { monPred_in_entails i : P1 i ⊢ P2 i }.
-Hint Immediate monPred_in_entails : core.
+Local Hint Immediate monPred_in_entails : core.
 
 Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index b8ab8b257..aa9906ef6 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -110,9 +110,9 @@ Section plainly_derived.
 Context `{BiPlainly PROP}.
 Implicit Types P : PROP.
 
-Hint Resolve pure_intro forall_intro : core.
-Hint Resolve or_elim or_intro_l' or_intro_r' : core.
-Hint Resolve and_intro and_elim_l' and_elim_r' : core.
+Local Hint Resolve pure_intro forall_intro : core.
+Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
+Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
 
 Global Instance plainly_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 11372d1c7..016e13f4c 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -10,10 +10,10 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Hint Resolve head_prim_reducible head_reducible_prim_step : core.
+Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
 Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
-Hint Resolve reducible_not_val_inhabitant : core.
-Hint Resolve head_stuck_stuck : core.
+Local Hint Resolve reducible_not_val_inhabitant : core.
+Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index c599f97c9..9649a8124 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -109,7 +109,7 @@ Section language.
        ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
        prim_step e1 σ1 κ e2 σ2 efs →
        step ρ1 κ ρ2.
-  Hint Constructors step : core.
+  Local Hint Constructors step : core.
 
   Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
     | nsteps_refl ρ :
@@ -118,7 +118,7 @@ Section language.
        step ρ1 κ ρ2 →
        nsteps n ρ2 κs ρ3 →
        nsteps (S n) ρ1 (κ ++ κs) ρ3.
-  Hint Constructors nsteps : core.
+  Local Hint Constructors nsteps : core.
 
   Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
 
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 9b532e703..04189b77f 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -14,7 +14,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Hint Resolve reducible_no_obs_reducible : core.
+Local Hint Resolve reducible_no_obs_reducible : core.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 9b8e438be..4c2ca48c5 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -210,10 +210,10 @@ Section ectx_lifting.
   Implicit Types s : stuckness.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
-  Hint Resolve head_prim_reducible head_reducible_prim_step : core.
+  Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
   Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
-  Hint Resolve reducible_not_val_inhabitant : core.
-  Hint Resolve head_stuck_stuck : core.
+  Local Hint Resolve reducible_not_val_inhabitant : core.
+  Local Hint Resolve head_stuck_stuck : core.
 
   Lemma ownP_lift_head_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ (ownP σ1) ∗
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 2d0d1043d..0f7147c5a 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -9,7 +9,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
+Local Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
   head_reducible_no_obs_reducible : core.
 
 Lemma twp_lift_head_step {s E Φ} e1 :
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index c1e4eb617..ba799dd8f 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -11,7 +11,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Hint Resolve reducible_no_obs_reducible : core.
+Local Hint Resolve reducible_no_obs_reducible : core.
 
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index fb132f827..02f3e6c48 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -90,7 +90,7 @@ Context {A : Type}.
 Implicit Types Γ : env A.
 Implicit Types i : ident.
 Implicit Types x : A.
-Hint Resolve Esnoc_wf Enil_wf : core.
+Local Hint Resolve Esnoc_wf Enil_wf : core.
 
 Ltac simplify :=
   repeat match goal with
-- 
GitLab