From e8d341beab2fd0711fcfba354d78c952b71cd3ef Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 27 Nov 2020 16:59:16 -0600
Subject: [PATCH] Add explicit Global to hints at top level
Fixes new Coq master warning deprecated-hint-without-locality
(https://github.com/coq/coq/pull/13188).
---
iris/algebra/cmra.v | 39 ++++-----
iris/algebra/ofe.v | 18 ++---
iris/algebra/proofmode_classes.v | 8 +-
iris/base_logic/bi.v | 2 +-
iris/base_logic/lib/iprop.v | 2 +-
iris/base_logic/lib/own.v | 2 +-
iris/base_logic/upred.v | 2 +-
iris/bi/derived_connectives.v | 14 ++--
iris/bi/embedding.v | 35 ++++----
iris/bi/interface.v | 2 +-
iris/bi/internal_eq.v | 4 +-
iris/bi/lib/fractional.v | 4 +-
iris/bi/lib/laterable.v | 2 +-
iris/bi/monpred.v | 2 +-
iris/bi/plainly.v | 14 ++--
iris/bi/updates.v | 14 ++--
iris/proofmode/class_instances.v | 4 +-
iris/proofmode/classes.v | 132 +++++++++++++++----------------
iris/proofmode/ident_name.v | 2 +-
iris/proofmode/ltac_tactics.v | 72 ++++++++---------
iris/proofmode/monpred.v | 16 ++--
iris/si_logic/bi.v | 2 +-
iris/si_logic/siprop.v | 2 +-
iris_heap_lang/primitive_laws.v | 4 +-
24 files changed, 200 insertions(+), 198 deletions(-)
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 3f8f002a1..6164660dc 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -3,11 +3,11 @@ From iris.algebra Require Export ofe monoid.
From iris.prelude Require Import options.
Class PCore (A : Type) := pcore : A → option A.
-Hint Mode PCore ! : typeclass_instances.
+Global Hint Mode PCore ! : typeclass_instances.
Instance: Params (@pcore) 2 := {}.
Class Op (A : Type) := op : A → A → A.
-Hint Mode Op ! : typeclass_instances.
+Global Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2 := {}.
Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
Notation "(â‹…)" := op (only parsing) : stdpp_scope.
@@ -20,17 +20,17 @@ Notation "(â‹…)" := op (only parsing) : stdpp_scope.
Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
-Hint Extern 0 (_ ≼ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≼ _) => reflexivity : core.
Instance: Params (@included) 3 := {}.
Class ValidN (A : Type) := validN : nat → A → Prop.
-Hint Mode ValidN ! : typeclass_instances.
+Global Hint Mode ValidN ! : typeclass_instances.
Instance: Params (@validN) 3 := {}.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A → Prop.
-Hint Mode Valid ! : typeclass_instances.
+Global Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
@@ -38,7 +38,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4 := {}.
-Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
+Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
Section mixin.
Local Set Primitive Projections.
@@ -93,10 +93,10 @@ Arguments cmra_validN : simpl never.
Arguments cmra_ofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
-Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
-Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
-Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
-Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
+Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
+Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
+Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
+Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
@@ -145,32 +145,32 @@ Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
Arguments core_id {_} _ {_}.
-Hint Mode CoreId + ! : typeclass_instances.
+Global Hint Mode CoreId + ! : typeclass_instances.
Instance: Params (@CoreId) 1 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
Arguments exclusive0_l {_} _ {_} _ _.
-Hint Mode Exclusive + ! : typeclass_instances.
+Global Hint Mode Exclusive + ! : typeclass_instances.
Instance: Params (@Exclusive) 1 := {}.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
Arguments cancelableN {_} _ {_} _ _ _ _.
-Hint Mode Cancelable + ! : typeclass_instances.
+Global Hint Mode Cancelable + ! : typeclass_instances.
Instance: Params (@Cancelable) 1 := {}.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
Arguments id_free0_r {_} _ {_} _ _.
-Hint Mode IdFree + ! : typeclass_instances.
+Global Hint Mode IdFree + ! : typeclass_instances.
Instance: Params (@IdFree) 1 := {}.
(** * CMRAs whose core is total *)
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
-Hint Mode CmraTotal ! : typeclass_instances.
+Global Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
@@ -215,7 +215,7 @@ Arguments ucmra_ofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
-Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
+Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
@@ -239,7 +239,7 @@ Class CmraDiscrete (A : cmraT) := {
cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
}.
-Hint Mode CmraDiscrete ! : typeclass_instances.
+Global Hint Mode CmraDiscrete ! : typeclass_instances.
(** * Morphisms *)
Class CmraMorphism {A B : cmraT} (f : A → B) := {
@@ -653,7 +653,7 @@ Section ucmra.
Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
End ucmra.
-Hint Immediate cmra_unit_cmra_total : core.
+Global Hint Immediate cmra_unit_cmra_total : core.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
@@ -1222,7 +1222,8 @@ Section prod.
End prod.
(* Registering as [Hint Extern] with new unification. *)
-Hint Extern 4 (CoreId _) => notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
+Global Hint Extern 4 (CoreId _) =>
+ notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
Arguments prodR : clear implicits.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 87f734ef5..04de827ca 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -19,8 +19,8 @@ Notation "x ≡{ n }≡ y" := (dist n x y)
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
(at level 70, n at next level, only parsing).
-Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
-Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
+Global Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
@@ -52,8 +52,8 @@ Structure ofeT := OfeT {
}.
Arguments OfeT _ {_ _} _.
Add Printing Constructor ofeT.
-Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
-Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
Arguments ofe_car : simpl never.
Arguments ofe_equiv : simpl never.
Arguments ofe_dist : simpl never.
@@ -96,12 +96,12 @@ Section ofe_mixin.
Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
End ofe_mixin.
-Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
+Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
(** Discrete OFEs and discrete OFE elements *)
Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
Arguments discrete {_} _ {_} _ _.
-Hint Mode Discrete + ! : typeclass_instances.
+Global Hint Mode Discrete + ! : typeclass_instances.
Instance: Params (@Discrete) 1 := {}.
Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
@@ -125,7 +125,7 @@ Class Cofe (A : ofeT) := {
conv_compl n c : compl c ≡{n}≡ c n;
}.
Arguments compl : simpl never.
-Hint Mode Cofe ! : typeclass_instances.
+Global Hint Mode Cofe ! : typeclass_instances.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
compl (chain_map f c) ≡ f (compl c).
@@ -258,7 +258,7 @@ Ltac solve_contractive :=
(** Limit preserving predicates *)
Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
-Hint Mode LimitPreserving + + ! : typeclass_instances.
+Global Hint Mode LimitPreserving + + ! : typeclass_instances.
Section limit_preserving.
Context `{Cofe A}.
@@ -716,7 +716,7 @@ Bind Scope oFunctor_scope with oFunctor.
Class oFunctorContractive (F : oFunctor) :=
oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Hint Mode oFunctorContractive ! : typeclass_instances.
+Global Hint Mode oFunctorContractive ! : typeclass_instances.
(** Not a coercion due to the [Cofe] type class argument, and to avoid
ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index efd07f08a..a04eb8692 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -17,18 +17,18 @@ From iris.prelude Require Import options.
*)
Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
Arguments is_op {_} _ _ _ {_}.
-Hint Mode IsOp + - - - : typeclass_instances.
+Global Hint Mode IsOp + - - - : typeclass_instances.
Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
Proof. by rewrite /IsOp. Qed.
Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
-Hint Mode IsOp' + ! - - : typeclass_instances.
-Hint Mode IsOp' + - ! ! : typeclass_instances.
+Global Hint Mode IsOp' + ! - - : typeclass_instances.
+Global Hint Mode IsOp' + - ! ! : typeclass_instances.
Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
-Hint Mode IsOp'LR + ! - - : typeclass_instances.
+Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index ad6814fb4..806f169d1 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -160,7 +160,7 @@ Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate uPred_affine : core.
+Global Hint Immediate uPred_affine : core.
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
Proof. exact: @plainly_exist_1. Qed.
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 36a4fdd4f..d91c4229d 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -88,7 +88,7 @@ search is only triggered if the arguments of [subG] do not contain evars. Since
instance search for [subG] is restrained, instances should persistently have [subG] as
their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
-Hint Mode subG ! + : typeclass_instances.
+Global Hint Mode subG ! + : typeclass_instances.
Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
Proof.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 5e9faf31e..49bee658b 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -20,7 +20,7 @@ Arguments inG_apply {_ _} _ _ {_}.
(** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
not want Coq to pick one arbitrarily. *)
-Hint Mode inG - ! : typeclass_instances.
+Global Hint Mode inG - ! : typeclass_instances.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index bdb236c4e..2cf522d11 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -245,7 +245,7 @@ Qed.
(** logical entailement *)
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
{ uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
-Hint Resolve uPred_mono : uPred_def.
+Global Hint Resolve uPred_mono : uPred_def.
(** logical connectives *)
Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 88e7dcca5..abdfdf596 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -16,7 +16,7 @@ Infix "∗-∗" := bi_wand_iff : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
-Hint Mode Persistent + ! : typeclass_instances.
+Global Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1 := {}.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
@@ -28,15 +28,15 @@ Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
-Hint Mode Affine + ! : typeclass_instances.
+Global Hint Mode Affine + ! : typeclass_instances.
Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Hint Mode BiAffine ! : typeclass_instances.
+Global Hint Mode BiAffine ! : typeclass_instances.
Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
-Hint Mode BiPositive ! : typeclass_instances.
+Global Hint Mode BiPositive ! : typeclass_instances.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
@@ -47,7 +47,7 @@ Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.
-Hint Mode Absorbing + ! : typeclass_instances.
+Global Hint Mode Absorbing + ! : typeclass_instances.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <pers> P else P)%I.
@@ -103,7 +103,7 @@ Typeclasses Opaque bi_except_0.
Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
-Hint Mode Timeless + ! : typeclass_instances.
+Global Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1 := {}.
(** An optional precondition [mP] to [Q].
@@ -128,7 +128,7 @@ The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [B
It is provided by the lemma [löb] in [derived_laws_later]. *)
Class BiLöb (PROP : bi) :=
löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
-Hint Mode BiLöb ! : typeclass_instances.
+Global Hint Mode BiLöb ! : typeclass_instances.
Arguments löb_weak {_ _} _ _.
Notation BiLaterContractive PROP :=
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 354028caa..c6532c198 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -12,8 +12,8 @@ Notation "⎡ P ⎤" := (embed P) : bi_scope.
Instance: Params (@embed) 3 := {}.
Typeclasses Opaque embed.
-Hint Mode Embed ! - : typeclass_instances.
-Hint Mode Embed - ! : typeclass_instances.
+Global Hint Mode Embed ! - : typeclass_instances.
+Global Hint Mode Embed - ! : typeclass_instances.
(* Mixins allow us to create instances easily without having to use Program *)
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
@@ -47,43 +47,43 @@ Class BiEmbed (PROP1 PROP2 : bi) := {
bi_embed_embed :> Embed PROP1 PROP2;
bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
-Hint Mode BiEmbed ! - : typeclass_instances.
-Hint Mode BiEmbed - ! : typeclass_instances.
+Global Hint Mode BiEmbed ! - : typeclass_instances.
+Global Hint Mode BiEmbed - ! : typeclass_instances.
Arguments bi_embed_embed : simpl never.
Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
-Hint Mode BiEmbedEmp ! - - : typeclass_instances.
-Hint Mode BiEmbedEmp - ! - : typeclass_instances.
+Global Hint Mode BiEmbedEmp ! - - : typeclass_instances.
+Global Hint Mode BiEmbedEmp - ! - : typeclass_instances.
Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤.
-Hint Mode BiEmbedLater ! - - : typeclass_instances.
-Hint Mode BiEmbedLater - ! - : typeclass_instances.
+Global Hint Mode BiEmbedLater ! - - : typeclass_instances.
+Global Hint Mode BiEmbedLater - ! - : typeclass_instances.
Class BiEmbedInternalEq (PROP1 PROP2 : bi)
`{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
-Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
-Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
Class BiEmbedBUpd (PROP1 PROP2 : bi)
`{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
-Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
-Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
Class BiEmbedFUpd (PROP1 PROP2 : bi)
`{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} :=
embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤.
-Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
-Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
Class BiEmbedPlainly (PROP1 PROP2 : bi)
`{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
embed_plainly (P : PROP1) : ⎡■P⎤ ⊣⊢@{PROP2} ■⎡P⎤.
-Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
-Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+Global Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
Section embed_laws.
Context `{BiEmbed PROP1 PROP2}.
@@ -315,4 +315,5 @@ End embed.
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [monPred_objectively_plain]
for an example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
+Global Hint Extern 4 (Plain _) =>
+ notypeclasses refine (embed_plain _ _) : typeclass_instances.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index f3f66ba4f..ca25529a2 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -217,7 +217,7 @@ Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_persistently {PROP} _%I : simpl never, rename.
Arguments bi_later {PROP} _%I : simpl never, rename.
-Hint Extern 0 (bi_entails _ _) => reflexivity : core.
+Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 4562e5871..593d7cf7f 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -9,7 +9,7 @@ can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
Class InternalEq (PROP : bi) :=
internal_eq : ∀ {A : ofeT}, A → A → PROP.
Arguments internal_eq {_ _ _} _ _ : simpl never.
-Hint Mode InternalEq ! : typeclass_instances.
+Global Hint Mode InternalEq ! : typeclass_instances.
Instance: Params (@internal_eq) 3 := {}.
Infix "≡" := internal_eq : bi_scope.
Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
@@ -40,7 +40,7 @@ Class BiInternalEq (PROP : bi) := {
bi_internal_eq_internal_eq :> InternalEq PROP;
bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
}.
-Hint Mode BiInternalEq ! : typeclass_instances.
+Global Hint Mode BiInternalEq ! : typeclass_instances.
Arguments bi_internal_eq_internal_eq : simpl never.
Section internal_eq_laws.
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 644c47ef2..0c84e2778 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -14,10 +14,10 @@ Arguments AsFractional {_} _%I _%I _%Qp.
Arguments fractional {_ _ _} _ _.
-Hint Mode AsFractional - + - - : typeclass_instances.
+Global Hint Mode AsFractional - + - - : typeclass_instances.
(* To make [as_fractional_fractional] a useful instance, we have to
allow [q] to be an evar. *)
-Hint Mode AsFractional - - + - : typeclass_instances.
+Global Hint Mode AsFractional - - + - : typeclass_instances.
Section fractional.
Context {PROP : bi}.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 1d11af00c..7c21a1e4b 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -7,7 +7,7 @@ Class Laterable {PROP : bi} (P : PROP) := laterable :
P -∗ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
Arguments Laterable {_} _%I : simpl never.
Arguments laterable {_} _%I {_}.
-Hint Mode Laterable + ! : typeclass_instances.
+Global Hint Mode Laterable + ! : typeclass_instances.
Section instances.
Context {PROP : bi}.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index d1f047eb4..bc1ca58ae 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -323,7 +323,7 @@ Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i -∗ P j.
Arguments Objective {_ _} _%I.
Arguments objective_at {_ _} _%I {_}.
-Hint Mode Objective + + ! : typeclass_instances.
+Global Hint Mode Objective + + ! : typeclass_instances.
Instance: Params (@Objective) 2 := {}.
(** Primitive facts that cannot be deduced from the BI structure. *)
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 4d2439693..b8ab8b257 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type*".
Class Plainly (A : Type) := plainly : A → A.
Arguments plainly {A}%type_scope {_} _%I.
-Hint Mode Plainly ! : typeclass_instances.
+Global Hint Mode Plainly ! : typeclass_instances.
Instance: Params (@plainly) 2 := {}.
Notation "â– P" := (plainly P) : bi_scope.
@@ -42,7 +42,7 @@ Class BiPlainly (PROP : bi) := {
bi_plainly_plainly :> Plainly PROP;
bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
}.
-Hint Mode BiPlainly ! : typeclass_instances.
+Global Hint Mode BiPlainly ! : typeclass_instances.
Arguments bi_plainly_plainly : simpl never.
Class BiPlainlyExist `{!BiPlainly PROP} :=
@@ -51,14 +51,14 @@ Class BiPlainlyExist `{!BiPlainly PROP} :=
Arguments BiPlainlyExist : clear implicits.
Arguments BiPlainlyExist _ {_}.
Arguments plainly_exist_1 _ {_ _} _.
-Hint Mode BiPlainlyExist ! - : typeclass_instances.
+Global Hint Mode BiPlainlyExist ! - : typeclass_instances.
Class BiPropExt `{!BiPlainly PROP, !BiInternalEq PROP} :=
prop_ext_2 (P Q : PROP) : ■(P ∗-∗ Q) ⊢ P ≡ Q.
Arguments BiPropExt : clear implicits.
Arguments BiPropExt _ {_ _}.
Arguments prop_ext_2 _ {_ _ _} _.
-Hint Mode BiPropExt ! - - : typeclass_instances.
+Global Hint Mode BiPropExt ! - - : typeclass_instances.
Section plainly_laws.
Context `{BiPlainly PROP}.
@@ -94,7 +94,7 @@ End plainly_laws.
Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■P.
Arguments Plain {_ _} _%I : simpl never.
Arguments plain {_ _} _%I {_}.
-Hint Mode Plain + - ! : typeclass_instances.
+Global Hint Mode Plain + - ! : typeclass_instances.
Instance: Params (@Plain) 1 := {}.
Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
@@ -644,11 +644,11 @@ apply it the instance at any node in the proof search tree.
To avoid that, we declare it using a [Hint Immediate], so that it will
only be used at the leaves of the proof search tree, i.e. when the
premise of the hint can be derived from just the current context. *)
-Hint Immediate plain_persistent : typeclass_instances.
+Global Hint Immediate plain_persistent : typeclass_instances.
(* Not defined using an ordinary [Instance] because the default
[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [coreP_persistent] for an
example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Persistent _) =>
+Global Hint Extern 4 (Persistent _) =>
notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 0dc792e34..e63610cde 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type*".
bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
Instance : Params (@bupd) 2 := {}.
-Hint Mode BUpd ! : typeclass_instances.
+Global Hint Mode BUpd ! : typeclass_instances.
Arguments bupd {_}%type_scope {_} _%bi_scope.
Notation "|==> Q" := (bupd Q) : bi_scope.
@@ -19,7 +19,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
Instance: Params (@fupd) 4 := {}.
-Hint Mode FUpd ! : typeclass_instances.
+Global Hint Mode FUpd ! : typeclass_instances.
Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
@@ -82,23 +82,23 @@ Class BiBUpd (PROP : bi) := {
bi_bupd_bupd :> BUpd PROP;
bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.
-Hint Mode BiBUpd ! : typeclass_instances.
+Global Hint Mode BiBUpd ! : typeclass_instances.
Arguments bi_bupd_bupd : simpl never.
Class BiFUpd (PROP : bi) := {
bi_fupd_fupd :> FUpd PROP;
bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
-Hint Mode BiFUpd ! : typeclass_instances.
+Global Hint Mode BiFUpd ! : typeclass_instances.
Arguments bi_fupd_fupd : simpl never.
Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
-Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
+Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
bupd_plainly (P : PROP) : (|==> ■P) -∗ P.
-Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
+Global Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
(** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
only make sense for affine logics. From the axioms below, one could derive
@@ -123,7 +123,7 @@ Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
(∀ x, |={E}=> ■Φ x) ⊢ |={E}=> ∀ x, Φ x
}.
-Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
+Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Section bupd_laws.
Context `{BiBUpd PROP}.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 8b5f315fb..6c2b00dcb 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -14,7 +14,7 @@ created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
[?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
-Hint Extern 0 (FromAssumption _ _ _) =>
+Global Hint Extern 0 (FromAssumption _ _ _) =>
notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
(* FIXME(Coq #6294): needs new unification *)
@@ -23,7 +23,7 @@ enable the better unification algorithm.
See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
-Hint Extern 0 (FromExist _ _) =>
+Global Hint Extern 0 (FromExist _ _) =>
notypeclasses refine (from_exist_exist _) : typeclass_instances.
Section class_instances.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index b71455cd7..51886c557 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -9,25 +9,25 @@ Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
from_assumption : □?p P ⊢ Q.
Arguments FromAssumption {_} _ _%I _%I : simpl never.
Arguments from_assumption {_} _ _%I _%I {_}.
-Hint Mode FromAssumption + + - - : typeclass_instances.
+Global Hint Mode FromAssumption + + - - : typeclass_instances.
Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
knownl_from_assumption :> FromAssumption p P Q.
Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
Arguments knownl_from_assumption {_} _ _%I _%I {_}.
-Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
+Global Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
knownr_from_assumption :> FromAssumption p P Q.
Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
Arguments knownr_from_assumption {_} _ _%I _%I {_}.
-Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
+Global Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
into_pure : P ⊢ ⌜φâŒ.
Arguments IntoPure {_} _%I _%type_scope : simpl never.
Arguments into_pure {_} _%I _%type_scope {_}.
-Hint Mode IntoPure + ! - : typeclass_instances.
+Global Hint Mode IntoPure + ! - : typeclass_instances.
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
@@ -53,7 +53,7 @@ Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
Proof. by exists φ. Qed.
-Hint Extern 0 (IntoPureT _ _) =>
+Global Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
(** [FromPure a P φ] is used when introducing a pure assertion. It is used by
@@ -69,27 +69,27 @@ Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
from_pure : <affine>?a ⌜φ⌠⊢ P.
Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}.
-Hint Mode FromPure + - ! - : typeclass_instances.
+Global Hint Mode FromPure + - ! - : typeclass_instances.
Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure a P ψ.
Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
FromPure a P φ → FromPureT a P φ.
Proof. by exists φ. Qed.
-Hint Extern 0 (FromPureT _ _ _) =>
+Global Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Class IntoInternalEq `{BiInternalEq PROP} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
-Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
+Global Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
into_persistent : <pers>?p P ⊢ <pers> Q.
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
-Hint Mode IntoPersistent + + ! - : typeclass_instances.
+Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
a goal [P] into a modality [M] and proposition [Q].
@@ -112,7 +112,7 @@ Class FromModal {PROP1 PROP2 : bi} {A}
from_modal : M Q ⊢ P.
Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
-Hint Mode FromModal - + - - - ! - : typeclass_instances.
+Global Hint Mode FromModal - + - - - ! - : typeclass_instances.
(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
proposition [Q].
@@ -122,7 +122,7 @@ Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : <affine> Q ⊢ P.
Arguments FromAffinely {_} _%I _%I : simpl never.
Arguments from_affinely {_} _%I _%I {_}.
-Hint Mode FromAffinely + - ! : typeclass_instances.
+Global Hint Mode FromAffinely + - ! : typeclass_instances.
(** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
the proposition [Q].
@@ -132,7 +132,7 @@ Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
into_absorbingly : P ⊢ <absorb> Q.
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
-Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
+Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
(** Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
@@ -146,86 +146,86 @@ Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
into_wand : □?p R ⊢ □?q P -∗ Q.
Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
Arguments into_wand {_} _ _ _%I _%I _%I {_}.
-Hint Mode IntoWand + + + ! - - : typeclass_instances.
+Global Hint Mode IntoWand + + + ! - - : typeclass_instances.
Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP) :=
into_wand' : IntoWand p q R P Q.
Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
-Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
-Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
+Global Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
+Global Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
Arguments FromWand {_} _%I _%I _%I : simpl never.
Arguments from_wand {_} _%I _%I _%I {_}.
-Hint Mode FromWand + ! - - : typeclass_instances.
+Global Hint Mode FromWand + ! - - : typeclass_instances.
Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
Arguments FromImpl {_} _%I _%I _%I : simpl never.
Arguments from_impl {_} _%I _%I _%I {_}.
-Hint Mode FromImpl + ! - - : typeclass_instances.
+Global Hint Mode FromImpl + ! - - : typeclass_instances.
Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
Arguments FromSep {_} _%I _%I _%I : simpl never.
Arguments from_sep {_} _%I _%I _%I {_}.
-Hint Mode FromSep + ! - - : typeclass_instances.
-Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
+Global Hint Mode FromSep + ! - - : typeclass_instances.
+Global Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
Arguments FromAnd {_} _%I _%I _%I : simpl never.
Arguments from_and {_} _%I _%I _%I {_}.
-Hint Mode FromAnd + ! - - : typeclass_instances.
-Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
+Global Hint Mode FromAnd + ! - - : typeclass_instances.
+Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
-Hint Mode IntoAnd + + ! - - : typeclass_instances.
+Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
into_sep : P ⊢ Q1 ∗ Q2.
Arguments IntoSep {_} _%I _%I _%I : simpl never.
Arguments into_sep {_} _%I _%I _%I {_}.
-Hint Mode IntoSep + ! - - : typeclass_instances.
+Global Hint Mode IntoSep + ! - - : typeclass_instances.
Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
Arguments FromOr {_} _%I _%I _%I : simpl never.
Arguments from_or {_} _%I _%I _%I {_}.
-Hint Mode FromOr + ! - - : typeclass_instances.
+Global Hint Mode FromOr + ! - - : typeclass_instances.
Class IntoOr {PROP : bi} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
Arguments IntoOr {_} _%I _%I _%I : simpl never.
Arguments into_or {_} _%I _%I _%I {_}.
-Hint Mode IntoOr + ! - - : typeclass_instances.
+Global Hint Mode IntoOr + ! - - : typeclass_instances.
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
from_exist : (∃ x, Φ x) ⊢ P.
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
-Hint Mode FromExist + - ! - : typeclass_instances.
+Global Hint Mode FromExist + - ! - : typeclass_instances.
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
into_exist : P ⊢ ∃ x, Φ x.
Arguments IntoExist {_ _} _%I _%I _ : simpl never.
Arguments into_exist {_ _} _%I _%I _ {_}.
-Hint Mode IntoExist + - ! - - : typeclass_instances.
+Global Hint Mode IntoExist + - ! - - : typeclass_instances.
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
into_forall : P ⊢ ∀ x, Φ x.
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
-Hint Mode IntoForall + - ! - : typeclass_instances.
+Global Hint Mode IntoForall + - ! - : typeclass_instances.
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
from_forall : (∀ x, Φ x) ⊢ P.
Arguments FromForall {_ _} _%I _%I _ : simpl never.
Arguments from_forall {_ _} _%I _%I _ {_}.
-Hint Mode FromForall + - ! - - : typeclass_instances.
+Global Hint Mode FromForall + - ! - - : typeclass_instances.
Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
-Hint Mode IsExcept0 + ! : typeclass_instances.
+Global Hint Mode IsExcept0 + ! : typeclass_instances.
(** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
@@ -250,7 +250,7 @@ Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP
elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
-Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
+Global Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
@@ -258,7 +258,7 @@ Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
add_modal : P ∗ (P' -∗ Q) ⊢ Q.
Arguments AddModal {_} _%I _%I _%I : simpl never.
Arguments add_modal {_} _%I _%I _%I {_}.
-Hint Mode AddModal + - ! ! : typeclass_instances.
+Global Hint Mode AddModal + - ! ! : typeclass_instances.
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
Proof. by rewrite /AddModal wand_elim_r. Qed.
@@ -279,7 +279,7 @@ Proof. done. Qed.
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_} _ _%I _%I _%I {_}.
-Hint Mode Frame + + ! ! - : typeclass_instances.
+Global Hint Mode Frame + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
@@ -288,7 +288,7 @@ Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
-Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
+Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
Frame p R P Q → MaybeFrame p R P Q true.
@@ -313,106 +313,106 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
Arguments MakeEmbed {_ _ _} _%I _%I.
-Hint Mode MakeEmbed + + + - - : typeclass_instances.
+Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
known_make_embed :> MakeEmbed P Q.
Arguments KnownMakeEmbed {_ _ _} _%I _%I.
-Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
+Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
Arguments MakeSep {_} _%I _%I _%I.
-Hint Mode MakeSep + - - - : typeclass_instances.
+Global Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownl_make_sep :> MakeSep P Q PQ.
Arguments KnownLMakeSep {_} _%I _%I _%I.
-Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownr_make_sep :> MakeSep P Q PQ.
Arguments KnownRMakeSep {_} _%I _%I _%I.
-Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
Class MakeAnd {PROP : bi} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
Arguments MakeAnd {_} _%I _%I _%I.
-Hint Mode MakeAnd + - - - : typeclass_instances.
+Global Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownl_make_and :> MakeAnd P Q PQ.
Arguments KnownLMakeAnd {_} _%I _%I _%I.
-Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownr_make_and :> MakeAnd P Q PQ.
Arguments KnownRMakeAnd {_} _%I _%I _%I.
-Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
Arguments MakeOr {_} _%I _%I _%I.
-Hint Mode MakeOr + - - - : typeclass_instances.
+Global Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
knownl_make_or :> MakeOr P Q PQ.
Arguments KnownLMakeOr {_} _%I _%I _%I.
-Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
+Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
Arguments KnownRMakeOr {_} _%I _%I _%I.
-Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
+Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
Arguments MakeAffinely {_} _%I _%I.
-Hint Mode MakeAffinely + - - : typeclass_instances.
+Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
known_make_affinely :> MakeAffinely P Q.
Arguments KnownMakeAffinely {_} _%I _%I.
-Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
+Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
Arguments MakeIntuitionistically {_} _%I _%I.
-Hint Mode MakeIntuitionistically + - - : typeclass_instances.
+Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
known_make_intuitionistically :> MakeIntuitionistically P Q.
Arguments KnownMakeIntuitionistically {_} _%I _%I.
-Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
+Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
Arguments MakeAbsorbingly {_} _%I _%I.
-Hint Mode MakeAbsorbingly + - - : typeclass_instances.
+Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
known_make_absorbingly :> MakeAbsorbingly P Q.
Arguments KnownMakeAbsorbingly {_} _%I _%I.
-Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
+Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
Arguments MakePersistently {_} _%I _%I.
-Hint Mode MakePersistently + - - : typeclass_instances.
+Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
known_make_persistently :> MakePersistently P Q.
Arguments KnownMakePersistently {_} _%I _%I.
-Hint Mode KnownMakePersistently + ! - : typeclass_instances.
+Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Arguments MakeLaterN {_} _%nat _%I _%I.
-Hint Mode MakeLaterN + + - - : typeclass_instances.
+Global Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
known_make_laterN :> MakeLaterN n P lP.
Arguments KnownMakeLaterN {_} _%nat _%I _%I.
-Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
+Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
Arguments MakeExcept0 {_} _%I _%I.
-Hint Mode MakeExcept0 + - - : typeclass_instances.
+Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
Arguments KnownMakeExcept0 {_} _%I _%I.
-Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
+Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
Arguments IntoExcept0 {_} _%I _%I : simpl never.
Arguments into_except_0 {_} _%I _%I {_}.
-Hint Mode IntoExcept0 + ! - : typeclass_instances.
-Hint Mode IntoExcept0 + - ! : typeclass_instances.
+Global Hint Mode IntoExcept0 + ! - : typeclass_instances.
+Global Hint Mode IntoExcept0 + - ! : typeclass_instances.
(* The class [MaybeIntoLaterN] has only two instances:
@@ -452,12 +452,12 @@ Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
maybe_into_laterN : P ⊢ ▷^n Q.
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
-Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
+Global Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN only_head n P Q.
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
-Hint Mode IntoLaterN + + + ! - : typeclass_instances.
+Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
MaybeIntoLaterN only_head n P P | 1000.
@@ -477,7 +477,7 @@ Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :
into_embed : P ⊢ ⎡Q⎤.
Arguments IntoEmbed {_ _ _} _%I _%I.
Arguments into_embed {_ _ _} _%I _%I {_}.
-Hint Mode IntoEmbed + + + ! - : typeclass_instances.
+Global Hint Mode IntoEmbed + + + ! - : typeclass_instances.
(* We use two type classes for [AsEmpValid], in order to avoid loops in
typeclass search. Indeed, the [as_emp_valid_embed] instance would try
@@ -510,7 +510,7 @@ Proof. by apply as_emp_valid. Qed.
Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
-Hint Mode IntoInv + ! - : typeclass_instances.
+Global Hint Mode IntoInv + ! - : typeclass_instances.
(** Accessors.
This definition only exists for the purpose of the proof mode; a truly
@@ -533,7 +533,7 @@ Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
-Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
+Global Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
(* Turn [P] into an accessor.
Inputs:
@@ -550,7 +550,7 @@ Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
-Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
+Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
(* The typeclass used for the [iInv] tactic.
Input: [Pinv]
@@ -578,7 +578,7 @@ Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
-Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
+Global Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
(** We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
diff --git a/iris/proofmode/ident_name.v b/iris/proofmode/ident_name.v
index 709205e3e..2457b844f 100644
--- a/iris/proofmode/ident_name.v
+++ b/iris/proofmode/ident_name.v
@@ -37,4 +37,4 @@ Ltac solve_as_ident_name :=
| _ => notypeclasses refine (to_ident_name __unknown)
end.
-Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
+Global Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 47127e687..af764cb9e 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1994,7 +1994,7 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
(** * Destruct tactic *)
Class CopyDestruct {PROP : bi} (P : PROP).
Arguments CopyDestruct {_} _%I.
-Hint Mode CopyDestruct + ! : typeclass_instances.
+Global Hint Mode CopyDestruct + ! : typeclass_instances.
Instance copy_destruct_forall {PROP : bi} {A} (Φ : A → PROP) : CopyDestruct (∀ x, Φ x) := {}.
Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
@@ -3261,54 +3261,54 @@ Tactic Notation "iAccu" :=
iStartProof; eapply tac_accu; [pm_reflexivity || fail "iAccu: not an evar"].
(** Automation *)
-Hint Extern 0 (_ ⊢ _) => iStartProof : core.
-Hint Extern 0 (⊢ _) => iStartProof : core.
+Global Hint Extern 0 (_ ⊢ _) => iStartProof : core.
+Global Hint Extern 0 (⊢ _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
-Hint Extern 0 (envs_entails _ ?Q) =>
+Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
+Global Hint Extern 0 (envs_entails _ ?Q) =>
first [is_evar Q; fail 1|iAssumption] : core.
-Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
+Global Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
-Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
+Global Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
rewrite envs_entails_eq; apply internal_eq_refl : core.
-Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepL_nil' _) : core.
-Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepL2_nil' _) : core.
-Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepM_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepM2_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepS_empty' _) : core.
-Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
+Global Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
rewrite envs_entails_eq; apply (big_sepMS_empty' _) : core.
(* These introduce as much as possible at once, for better performance. *)
-Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
-Hint Extern 0 (envs_entails _ (_ → _)) => iIntros : core.
-Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (_ → _)) => iIntros : core.
+Global Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros : core.
(* Multi-intro doesn't work for custom binders. *)
-Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
-
-Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
-Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
-Hint Extern 1 (envs_entails _ (â– _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (â–¡ _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.
-Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.
-Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft : core.
-Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight : core.
-Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro : core.
-Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.
-Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.
-
-Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
+Global Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
+
+Global Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
+Global Hint Extern 1 (envs_entails _ (â– _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (â–¡ _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.
+Global Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.
+Global Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft : core.
+Global Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight : core.
+Global Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro : core.
+Global Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.
+Global Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.
+
+Global Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index f59f09245..0b6b1df2f 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -10,13 +10,13 @@ Arguments MakeMonPredAt {_ _} _ _%I _%I.
(** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
important to use the mode [!] also for the first two arguments. *)
-Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
+Global Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
-Hint Mode IsBiIndexRel + - - : typeclass_instances.
+Global Hint Mode IsBiIndexRel + - - : typeclass_instances.
Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
Proof. by rewrite /IsBiIndexRel. Qed.
-Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
+Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
: typeclass_instances.
(** Frame [ð“¡] into the goal [monPred_at P i] and determine the remainder [ð“ ].
@@ -25,7 +25,7 @@ Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
(ð“¡ : PROP) (P : monPred I PROP) (ð“ : PROP) :=
frame_monPred_at : â–¡?p 𓡠∗ ð“ -∗ P i.
Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
-Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
+Global Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
Section modalities.
Context {I : biIndex} {PROP : bi}.
@@ -537,17 +537,17 @@ End bi.
As a result, depending on P and Q being evars, we use a different
version of [into_wand_monPred_at_xx_xx]. *)
-Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
+Global Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
is_evar P; is_evar Q;
eapply @into_wand_monPred_at_unknown_unknown
: typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
eapply @into_wand_monPred_at_unknown_known
: typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
eapply @into_wand_monPred_at_known_unknown_le
: typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+Global Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
eapply @into_wand_monPred_at_known_unknown_ge
: typeclass_instances.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index dc8be0254..375630f1d 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -163,7 +163,7 @@ Global Instance siProp_affine : BiAffine siPropI | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate siProp_affine : core.
+Global Hint Immediate siProp_affine : core.
Global Instance siProp_plain (P : siProp) : Plain P | 0.
Proof. done. Qed.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 345994a21..f47bbc7d0 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -53,7 +53,7 @@ End cofe.
(** logical entailement *)
Inductive siProp_entails (P Q : siProp) : Prop :=
{ siProp_in_entails : ∀ n, P n → Q n }.
-Hint Resolve siProp_closed : siProp_def.
+Global Hint Resolve siProp_closed : siProp_def.
(** logical connectives *)
Program Definition siProp_pure_def (φ : Prop) : siProp :=
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 36deec1e8..1caa75916 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -169,9 +169,9 @@ To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
as_recv : v = RecV f x erec.
-Hint Mode AsRecV ! - - - : typeclass_instances.
+Global Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
-Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
+Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
apply AsRecV_recv : typeclass_instances.
Instance pure_recc f x (erec : expr) :
--
GitLab