Verified Commit e8d341be authored by Tej Chajed's avatar Tej Chajed
Browse files

Add explicit Global to hints at top level

Fixes new Coq master warning deprecated-hint-without-locality
(https://github.com/coq/coq/pull/13188).
parent f0f9f3b6
......@@ -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.
......
......@@ -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. *)
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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 :=
......
......@@ -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 :=
......
......@@ -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.
......@@ -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).
......
......@@ -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.
......
......@@ -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}.
......
......@@ -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}.
......
......@@ -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. *)
......
......@@ -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.
......@@ -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.