From 79a110823166f989e622c8cdf1a8d564cc2078fd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jan 2021 13:51:26 +0100
Subject: [PATCH] also add Local/Global to Arguments
---
iris/algebra/agree.v | 8 +-
iris/algebra/big_op.v | 8 +-
iris/algebra/cmra.v | 74 +++++-----
iris/algebra/coPset.v | 2 +-
iris/algebra/cofe_solver.v | 4 +-
iris/algebra/csum.v | 10 +-
iris/algebra/dra.v | 24 ++--
iris/algebra/excl.v | 8 +-
iris/algebra/gmap.v | 6 +-
iris/algebra/gmultiset.v | 6 +-
iris/algebra/gset.v | 24 ++--
iris/algebra/list.v | 6 +-
iris/algebra/namespace_map.v | 12 +-
iris/algebra/ofe.v | 58 ++++----
iris/algebra/proofmode_classes.v | 2 +-
iris/algebra/sts.v | 16 +--
iris/algebra/vector.v | 2 +-
iris/algebra/view.v | 10 +-
iris/base_logic/lib/auth.v | 2 +-
iris/base_logic/lib/fancy_updates.v | 2 +-
iris/base_logic/lib/gen_heap.v | 6 +-
iris/base_logic/lib/gen_inv_heap.v | 6 +-
iris/base_logic/lib/ghost_var.v | 2 +-
iris/base_logic/lib/gset_bij.v | 4 +-
iris/base_logic/lib/invariants.v | 2 +-
iris/base_logic/lib/iprop.v | 2 +-
iris/base_logic/lib/mono_nat.v | 4 +-
iris/base_logic/lib/own.v | 24 ++--
iris/base_logic/lib/proph_map.v | 2 +-
iris/base_logic/lib/viewshifts.v | 2 +-
iris/base_logic/lib/wsat.v | 2 +-
iris/base_logic/upred.v | 36 ++---
iris/bi/big_op.v | 4 +-
iris/bi/derived_connectives.v | 42 +++---
iris/bi/embedding.v | 4 +-
iris/bi/interface.v | 32 ++---
iris/bi/internal_eq.v | 4 +-
iris/bi/lib/atomic.v | 6 +-
iris/bi/lib/counterexamples.v | 6 +-
iris/bi/lib/fixpoint.v | 6 +-
iris/bi/lib/fractional.v | 6 +-
iris/bi/lib/laterable.v | 4 +-
iris/bi/monpred.v | 22 +--
iris/bi/plainly.v | 22 +--
iris/bi/telescopes.v | 4 +-
iris/bi/updates.v | 8 +-
iris/bi/weakestpre.v | 4 +-
iris/program_logic/ectx_language.v | 16 +--
iris/program_logic/ectxi_language.v | 14 +-
iris/program_logic/language.v | 8 +-
iris/program_logic/total_weakestpre.v | 2 +-
iris/program_logic/weakestpre.v | 2 +-
iris/proofmode/base.v | 6 +-
iris/proofmode/classes.v | 192 +++++++++++++-------------
iris/proofmode/coq_tactics.v | 4 +-
iris/proofmode/environments.v | 16 +--
iris/proofmode/ident_name.v | 2 +-
iris/proofmode/ltac_tactics.v | 2 +-
iris/proofmode/modalities.v | 16 +--
iris/proofmode/monpred.v | 4 +-
iris/proofmode/notation.v | 6 +-
iris/si_logic/siprop.v | 4 +-
iris_heap_lang/lang.v | 6 +-
iris_heap_lang/lib/atomic_heap.v | 2 +-
iris_heap_lang/lib/lock.v | 10 +-
tests/heapprop.v | 2 +-
tests/ipm_paper.v | 6 +-
67 files changed, 435 insertions(+), 435 deletions(-)
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index bfc1a913b..6c938682a 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -34,8 +34,8 @@ Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
-Arguments agree_car {_} _.
-Arguments agree_not_nil {_} _.
+Global Arguments agree_car {_} _.
+Global Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Definition to_agree {A} (a : A) : agree A :=
@@ -259,8 +259,8 @@ Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
End agree.
Global Instance: Params (@to_agree) 1 := {}.
-Arguments agreeO : clear implicits.
-Arguments agreeR : clear implicits.
+Global Arguments agreeO : clear implicits.
+Global Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
{| agree_car := f <$> agree_car x |}.
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 6302c29f1..892e13a6e 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -26,7 +26,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Global Instance: Params (@big_opL) 4 := {}.
-Arguments big_opL {M} o {_ A} _ !_ /.
+Global Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
@@ -39,7 +39,7 @@ Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
-Arguments big_opM {M} o {_ K _ _ A} _ _.
+Global Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Global Instance: Params (@big_opM) 7 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
@@ -53,7 +53,7 @@ Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
-Arguments big_opS {M} o {_ A _ _} _ _.
+Global Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Global Instance: Params (@big_opS) 6 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
@@ -64,7 +64,7 @@ Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
-Arguments big_opMS {M} o {_ A _ _} _ _.
+Global Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Global Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 4cc21f60f..cc705a746 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -77,21 +77,21 @@ Structure cmraT := CmraT' {
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
-Arguments CmraT' _ {_ _ _ _ _ _} _ _.
+Global Arguments CmraT' _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m) (only parsing).
-Arguments cmra_car : simpl never.
-Arguments cmra_equiv : simpl never.
-Arguments cmra_dist : simpl never.
-Arguments cmra_pcore : simpl never.
-Arguments cmra_op : simpl never.
-Arguments cmra_valid : simpl never.
-Arguments cmra_validN : simpl never.
-Arguments cmra_ofe_mixin : simpl never.
-Arguments cmra_mixin : simpl never.
+Global Arguments cmra_car : simpl never.
+Global Arguments cmra_equiv : simpl never.
+Global Arguments cmra_dist : simpl never.
+Global Arguments cmra_pcore : simpl never.
+Global Arguments cmra_op : simpl never.
+Global Arguments cmra_valid : simpl never.
+Global Arguments cmra_validN : simpl never.
+Global Arguments cmra_ofe_mixin : simpl never.
+Global Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
@@ -144,27 +144,27 @@ 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 {_} _ {_}.
+Global Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
Global 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 {_} _ {_} _ _.
+Global Arguments exclusive0_l {_} _ {_} _ _.
Global Hint Mode Exclusive + ! : typeclass_instances.
Global 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 {_} _ {_} _ _ _ _.
+Global Arguments cancelableN {_} _ {_} _ _ _ _.
Global Hint Mode Cancelable + ! : typeclass_instances.
Global 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 {_} _ {_} _ _.
+Global Arguments id_free0_r {_} _ {_} _ _.
Global Hint Mode IdFree + ! : typeclass_instances.
Global Instance: Params (@IdFree) 1 := {}.
@@ -180,7 +180,7 @@ Global Instance: Params (@core) 2 := {}.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
-Arguments ε {_ _}.
+Global Arguments ε {_ _}.
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
@@ -201,19 +201,19 @@ Structure ucmraT := UcmraT' {
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
-Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
+Global Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
Notation UcmraT A m :=
(UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
-Arguments ucmra_car : simpl never.
-Arguments ucmra_equiv : simpl never.
-Arguments ucmra_dist : simpl never.
-Arguments ucmra_pcore : simpl never.
-Arguments ucmra_op : simpl never.
-Arguments ucmra_valid : simpl never.
-Arguments ucmra_validN : simpl never.
-Arguments ucmra_ofe_mixin : simpl never.
-Arguments ucmra_cmra_mixin : simpl never.
-Arguments ucmra_mixin : simpl never.
+Global Arguments ucmra_car : simpl never.
+Global Arguments ucmra_equiv : simpl never.
+Global Arguments ucmra_dist : simpl never.
+Global Arguments ucmra_pcore : simpl never.
+Global Arguments ucmra_op : simpl never.
+Global Arguments ucmra_valid : simpl never.
+Global Arguments ucmra_validN : simpl never.
+Global Arguments ucmra_ofe_mixin : simpl never.
+Global Arguments ucmra_cmra_mixin : simpl never.
+Global Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
@@ -248,9 +248,9 @@ Class CmraMorphism {A B : cmraT} (f : A → B) := {
cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.
-Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
-Arguments cmra_morphism_pcore {_ _} _ {_} _.
-Arguments cmra_morphism_op {_ _} _ {_} _ _.
+Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
+Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
+Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
(** * Properties **)
Section cmra.
@@ -1110,7 +1110,7 @@ Section prod.
Local Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
Local Instance prod_pcore : PCore (A * B) := λ x,
c1 ↠pcore (x.1); c2 ↠pcore (x.2); Some (c1, c2).
- Arguments prod_pcore !_ /.
+ Local Arguments prod_pcore !_ /.
Local Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
Local Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
@@ -1225,7 +1225,7 @@ End prod.
Global Hint Extern 4 (CoreId _) =>
notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
-Arguments prodR : clear implicits.
+Global Arguments prodR : clear implicits.
Section prod_unit.
Context {A B : ucmraT}.
@@ -1262,7 +1262,7 @@ Section prod_unit.
Proof. unfold_leibniz. apply pair_op_2. Qed.
End prod_unit.
-Arguments prodUR : clear implicits.
+Global Arguments prodUR : clear implicits.
Global Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
@@ -1338,7 +1338,7 @@ Section option.
Local Instance option_validN : ValidN (option A) := λ n ma,
match ma with Some a => ✓{n} a | None => True end.
Local Instance option_pcore : PCore (option A) := λ ma, Some (ma ≫= pcore).
- Arguments option_pcore !_ /.
+ Local Arguments option_pcore !_ /.
Local Instance option_op : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
@@ -1514,8 +1514,8 @@ Section option.
Proof. destruct ma; apply _. Qed.
End option.
-Arguments optionR : clear implicits.
-Arguments optionUR : clear implicits.
+Global Arguments optionR : clear implicits.
+Global Arguments optionUR : clear implicits.
Section option_prod.
Context {A B : cmraT}.
@@ -1659,8 +1659,8 @@ Section discrete_fun_cmra.
Proof. intros ? f Hf x. by apply: discrete. Qed.
End discrete_fun_cmra.
-Arguments discrete_funR {_} _.
-Arguments discrete_funUR {_} _.
+Global Arguments discrete_funR {_} _.
+Global Arguments discrete_funUR {_} _.
Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
(∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v
index 69f257c4b..8763d0d30 100644
--- a/iris/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -66,7 +66,7 @@ Inductive coPset_disj :=
| CoPsetBot : coPset_disj.
Section coPset_disj.
- Arguments op _ _ !_ !_ /.
+ Local Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid : Valid coPset_disj := λ X,
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 424fcedc1..4a2c745cd 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -28,8 +28,8 @@ with g (k : nat) : A (S k) -n> A k :=
match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
-Arguments f : simpl never.
-Arguments g : simpl never.
+Global Arguments f : simpl never.
+Global Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
Proof using Fcontr.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 23a2bc2be..8ff770410 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -13,9 +13,9 @@ Inductive csum (A B : Type) :=
| Cinl : A → csum A B
| Cinr : B → csum A B
| CsumBot : csum A B.
-Arguments Cinl {_ _} _.
-Arguments Cinr {_ _} _.
-Arguments CsumBot {_ _}.
+Global Arguments Cinl {_ _} _.
+Global Arguments Cinr {_ _} _.
+Global Arguments CsumBot {_ _}.
Global Instance: Params (@Cinl) 2 := {}.
Global Instance: Params (@Cinr) 2 := {}.
@@ -110,7 +110,7 @@ Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
End ofe.
-Arguments csumO : clear implicits.
+Global Arguments csumO : clear implicits.
(* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
@@ -361,7 +361,7 @@ Proof.
Qed.
End cmra.
-Arguments csumR : clear implicits.
+Global Arguments csumR : clear implicits.
(* Functor *)
Global Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index ee2b110ca..af0baf70e 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -35,14 +35,14 @@ Structure draT := DraT {
dra_valid : Valid dra_car;
dra_mixin : DraMixin dra_car
}.
-Arguments DraT _ {_ _ _ _ _} _.
-Arguments dra_car : simpl never.
-Arguments dra_equiv : simpl never.
-Arguments dra_pcore : simpl never.
-Arguments dra_disjoint : simpl never.
-Arguments dra_op : simpl never.
-Arguments dra_valid : simpl never.
-Arguments dra_mixin : simpl never.
+Global Arguments DraT _ {_ _ _ _ _} _.
+Global Arguments dra_car : simpl never.
+Global Arguments dra_equiv : simpl never.
+Global Arguments dra_pcore : simpl never.
+Global Arguments dra_disjoint : simpl never.
+Global Arguments dra_op : simpl never.
+Global Arguments dra_valid : simpl never.
+Global Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
@@ -93,9 +93,9 @@ Record validity (A : draT) := Validity {
validity_prf : validity_is_valid → valid validity_car
}.
Add Printing Constructor validity.
-Arguments Validity {_} _ _ _.
-Arguments validity_car {_} _.
-Arguments validity_is_valid {_} _.
+Global Arguments Validity {_} _ _ _.
+Global Arguments validity_car {_} _.
+Global Arguments validity_is_valid {_} _.
Definition to_validity {A : draT} (x : A) : validity A :=
Validity x (valid x) id.
@@ -105,7 +105,7 @@ Section dra.
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
-Arguments valid _ _ !_ /.
+Local Arguments valid _ _ !_ /.
Local Instance validity_valid : Valid (validity A) := validity_is_valid.
Local Instance validity_equiv : Equiv (validity A) := λ x y,
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index a54699658..655c6315d 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -7,8 +7,8 @@ Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A → excl A
| ExclBot : excl A.
-Arguments Excl {_} _.
-Arguments ExclBot {_}.
+Global Arguments Excl {_} _.
+Global Arguments ExclBot {_}.
Global Instance: Params (@Excl) 1 := {}.
Global Instance: Params (@ExclBot) 1 := {}.
@@ -114,8 +114,8 @@ Proof.
Qed.
End excl.
-Arguments exclO : clear implicits.
-Arguments exclR : clear implicits.
+Global Arguments exclO : clear implicits.
+Global Arguments exclR : clear implicits.
(* Functor *)
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 89fc7ad19..f41d0cbe7 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -97,7 +97,7 @@ Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
End ofe.
-Arguments gmapO _ {_ _} _.
+Global Arguments gmapO _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A → option B → option C)
@@ -232,8 +232,8 @@ Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
End cmra.
-Arguments gmapR _ {_ _} _.
-Arguments gmapUR _ {_ _} _.
+Global Arguments gmapR _ {_ _} _.
+Global Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
diff --git a/iris/algebra/gmultiset.v b/iris/algebra/gmultiset.v
index 2cacca3c8..02c3aa9f1 100644
--- a/iris/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -95,6 +95,6 @@ Section gmultiset.
End gmultiset.
-Arguments gmultisetO _ {_ _}.
-Arguments gmultisetR _ {_ _}.
-Arguments gmultisetUR _ {_ _}.
+Global Arguments gmultisetO _ {_ _}.
+Global Arguments gmultisetR _ {_ _}.
+Global Arguments gmultisetUR _ {_ _}.
diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 18d129bb5..6ad3aecba 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -66,22 +66,22 @@ Section gset.
End gset.
-Arguments gsetO _ {_ _}.
-Arguments gsetR _ {_ _}.
-Arguments gsetUR _ {_ _}.
+Global Arguments gsetO _ {_ _}.
+Global Arguments gsetR _ {_ _}.
+Global Arguments gsetUR _ {_ _}.
(* The disjoint union CMRA *)
Inductive gset_disj K `{Countable K} :=
| GSet : gset K → gset_disj K
| GSetBot : gset_disj K.
-Arguments GSet {_ _ _} _.
-Arguments GSetBot {_ _ _}.
+Global Arguments GSet {_ _ _} _.
+Global Arguments GSetBot {_ _ _}.
Section gset_disj.
Context `{Countable K}.
- Arguments op _ _ !_ !_ /.
- Arguments cmra_op _ !_ !_ /.
- Arguments ucmra_op _ !_ !_ /.
+ Local Arguments op _ _ !_ !_ /.
+ Local Arguments cmra_op _ !_ !_ /.
+ Local Arguments ucmra_op _ !_ !_ /.
Canonical Structure gset_disjO := leibnizO (gset_disj K).
@@ -134,7 +134,7 @@ Section gset_disj.
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
- Arguments op _ _ _ _ : simpl never.
+ Local Arguments op _ _ _ _ : simpl never.
Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
(∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
@@ -231,6 +231,6 @@ Section gset_disj.
Qed.
End gset_disj.
-Arguments gset_disjO _ {_ _}.
-Arguments gset_disjR _ {_ _}.
-Arguments gset_disjUR _ {_ _}.
+Global Arguments gset_disjO _ {_ _}.
+Global Arguments gset_disjR _ {_ _}.
+Global Arguments gset_disjUR _ {_ _}.
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 9666d5a09..1fac28aea 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -95,7 +95,7 @@ Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
End ofe.
-Arguments listO : clear implicits.
+Global Arguments listO : clear implicits.
(** Non-expansiveness of higher-order list functions and big-ops *)
Global Instance list_fmap_ne {A B : ofeT} (f : A → B) n :
@@ -296,8 +296,8 @@ Section cmra.
End cmra.
-Arguments listR : clear implicits.
-Arguments listUR : clear implicits.
+Global Arguments listR : clear implicits.
+Global Arguments listUR : clear implicits.
Global Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ε ++ [x].
diff --git a/iris/algebra/namespace_map.v b/iris/algebra/namespace_map.v
index 100e6dde4..862a60668 100644
--- a/iris/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -20,9 +20,9 @@ Record namespace_map (A : Type) := NamespaceMap {
namespace_map_token_proj : coPset_disj
}.
Add Printing Constructor namespace_map.
-Arguments NamespaceMap {_} _ _.
-Arguments namespace_map_data_proj {_} _.
-Arguments namespace_map_token_proj {_} _.
+Global Arguments NamespaceMap {_} _ _.
+Global Arguments namespace_map_data_proj {_} _.
+Global Arguments namespace_map_token_proj {_} _.
Global Instance: Params (@NamespaceMap) 1 := {}.
Global Instance: Params (@namespace_map_data_proj) 1 := {}.
Global Instance: Params (@namespace_map_token_proj) 1 := {}.
@@ -72,7 +72,7 @@ Global Instance namespace_map_ofe_discrete :
Proof. intros ? [??]; apply _. Qed.
End ofe.
-Arguments namespace_mapO : clear implicits.
+Global Arguments namespace_mapO : clear implicits.
(* Camera *)
Section cmra.
@@ -296,5 +296,5 @@ Proof.
Qed.
End cmra.
-Arguments namespace_mapR : clear implicits.
-Arguments namespace_mapUR : clear implicits.
+Global Arguments namespace_mapR : clear implicits.
+Global Arguments namespace_mapUR : clear implicits.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index f8b949fdb..9d0de0012 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -50,14 +50,14 @@ Structure ofeT := OfeT {
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
-Arguments OfeT _ {_ _} _.
+Global Arguments OfeT _ {_ _} _.
Add Printing Constructor ofeT.
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.
-Arguments ofe_mixin : simpl never.
+Global Arguments ofe_car : simpl never.
+Global Arguments ofe_equiv : simpl never.
+Global Arguments ofe_dist : simpl never.
+Global Arguments ofe_mixin : simpl never.
(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
@@ -100,7 +100,7 @@ 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 {_} _ {_} _ _.
+Global Arguments discrete {_} _ {_} _ _.
Global Hint Mode Discrete + ! : typeclass_instances.
Global Instance: Params (@Discrete) 1 := {}.
@@ -111,8 +111,8 @@ Record chain (A : ofeT) := {
chain_car :> nat → A;
chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
}.
-Arguments chain_car {_} _ _.
-Arguments chain_cauchy {_} _ _ _ _.
+Global Arguments chain_car {_} _ _.
+Global Arguments chain_cauchy {_} _ _ _ _.
Program Definition chain_map {A B : ofeT} (f : A → B)
`{!NonExpansive f} (c : chain A) : chain B :=
@@ -124,7 +124,7 @@ Class Cofe (A : ofeT) := {
compl : Compl A;
conv_compl n c : compl c ≡{n}≡ c n;
}.
-Arguments compl : simpl never.
+Global Arguments compl : simpl never.
Global Hint Mode Cofe ! : typeclass_instances.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
@@ -200,7 +200,7 @@ End ofe.
(** Contractive functions *)
Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x ≡{n}≡ y end.
-Arguments dist_later _ _ !_ _ _ /.
+Global Arguments dist_later _ _ !_ _ _ /.
Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
@@ -321,7 +321,7 @@ Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Definition fixpoint := fixpoint_aux.(unseal).
-Arguments fixpoint {A _ _} f {_}.
+Global Arguments fixpoint {A _ _} f {_}.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
@@ -529,7 +529,7 @@ Record ofe_mor (A B : ofeT) : Type := OfeMor {
ofe_mor_car :> A → B;
ofe_mor_ne : NonExpansive ofe_mor_car
}.
-Arguments OfeMor {_ _} _ {_}.
+Global Arguments OfeMor {_ _} _ {_}.
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
@@ -581,7 +581,7 @@ Section ofe_mor.
Proof. done. Qed.
End ofe_mor.
-Arguments ofe_morO : clear implicits.
+Global Arguments ofe_morO : clear implicits.
Notation "A -n> B" :=
(ofe_morO A B) (at level 99, B at level 200, right associativity).
Global Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
@@ -680,7 +680,7 @@ Section product.
Proof. intros ?? [??]; apply _. Qed.
End product.
-Arguments prodO : clear implicits.
+Global Arguments prodO : clear implicits.
Typeclasses Opaque prod_dist.
Global Instance prod_map_ne {A A' B B' : ofeT} n :
@@ -872,7 +872,7 @@ Section sum.
Proof. intros ?? [?|?]; apply _. Qed.
End sum.
-Arguments sumO : clear implicits.
+Global Arguments sumO : clear implicits.
Typeclasses Opaque sum_dist.
Global Instance sum_map_ne {A A' B B' : ofeT} n :
@@ -1035,7 +1035,7 @@ Section option.
End option.
Typeclasses Opaque option_dist.
-Arguments optionO : clear implicits.
+Global Arguments optionO : clear implicits.
Global Instance option_fmap_ne {A B : ofeT} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
@@ -1089,8 +1089,8 @@ If you need to get a witness out, you should use the lemma [Next_uninj]
instead. *)
Record later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
-Arguments Next {_} _.
-Arguments later_car {_} _.
+Global Arguments Next {_} _.
+Global Arguments later_car {_} _.
Global Instance: Params (@Next) 1 := {}.
Section later.
@@ -1144,7 +1144,7 @@ Section later.
Qed.
End later.
-Arguments laterO : clear implicits.
+Global Arguments laterO : clear implicits.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
Next (f (later_car x)).
@@ -1249,7 +1249,7 @@ Section discrete_fun.
Qed.
End discrete_fun.
-Arguments discrete_funO {_} _.
+Global Arguments discrete_funO {_} _.
Notation "A -d> B" :=
(@discrete_funO A (λ _, B)) (at level 99, B at level 200, right associativity).
@@ -1381,7 +1381,7 @@ Section sigma.
Proof. intros ??. apply _. Qed.
End sigma.
-Arguments sigO {_} _.
+Global Arguments sigO {_} _.
(** * SigmaT type *)
(** Ofe for [sigT]. The first component must be discrete and use Leibniz
@@ -1541,7 +1541,7 @@ Section sigT.
End cofe.
End sigT.
-Arguments sigTO {_} _.
+Global Arguments sigTO {_} _.
Section sigTOF.
Context {A : Type}.
@@ -1578,7 +1578,7 @@ Section sigTOF.
repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
Qed.
End sigTOF.
-Arguments sigTOF {_} _%OF.
+Global Arguments sigTOF {_} _%OF.
Notation "{ x & P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
Notation "{ x : A & P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
@@ -1590,11 +1590,11 @@ Record ofe_iso (A B : ofeT) := OfeIso {
ofe_iso_12 y : ofe_iso_1 (ofe_iso_2 y) ≡ y;
ofe_iso_21 x : ofe_iso_2 (ofe_iso_1 x) ≡ x;
}.
-Arguments OfeIso {_ _} _ _ _ _.
-Arguments ofe_iso_1 {_ _} _.
-Arguments ofe_iso_2 {_ _} _.
-Arguments ofe_iso_12 {_ _} _ _.
-Arguments ofe_iso_21 {_ _} _ _.
+Global Arguments OfeIso {_ _} _ _ _ _.
+Global Arguments ofe_iso_1 {_ _} _.
+Global Arguments ofe_iso_2 {_ _} _.
+Global Arguments ofe_iso_12 {_ _} _ _.
+Global Arguments ofe_iso_21 {_ _} _ _.
Section ofe_iso.
Context {A B : ofeT}.
@@ -1626,7 +1626,7 @@ Section ofe_iso.
Qed.
End ofe_iso.
-Arguments ofe_isoO : clear implicits.
+Global Arguments ofe_isoO : clear implicits.
Program Definition iso_ofe_refl {A} : ofe_iso A A := OfeIso cid cid _ _.
Solve Obligations with done.
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 26fedca2d..0f1ab34e7 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -16,7 +16,7 @@ From iris.prelude Require Import options.
[own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
*)
Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
-Arguments is_op {_} _ _ _ {_}.
+Global Arguments is_op {_} _ _ _ {_}.
Global Hint Mode IsOp + - - - : typeclass_instances.
Global Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 440147127..707deaece 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -20,9 +20,9 @@ Structure stsT := Sts {
prim_step : relation state;
tok : state → propset token;
}.
-Arguments Sts {_ _} _ _.
-Arguments prim_step {_} _ _.
-Arguments tok {_} _.
+Global Arguments Sts {_ _} _ _.
+Global Arguments prim_step {_} _ _.
+Global Arguments tok {_} _.
Notation states sts := (propset (state sts)).
Notation tokens sts := (propset (token sts)).
@@ -179,8 +179,8 @@ Notation frame_steps T := (rtc (frame_step T)).
Inductive car (sts : stsT) :=
| auth : state sts → propset (token sts) → car sts
| frag : propset (state sts) → propset (token sts) → car sts.
-Arguments auth {_} _ _.
-Arguments frag {_} _ _.
+Global Arguments auth {_} _ _.
+Global Arguments frag {_} _ _.
End sts.
Notation stsT := sts.stsT.
@@ -300,7 +300,7 @@ Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.
-Arguments dra_valid _ !_/.
+Local Arguments dra_valid _ !_/.
(** Setoids *)
Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
@@ -461,8 +461,8 @@ Structure stsT := Sts {
state : Type;
prim_step : relation state;
}.
-Arguments Sts {_} _.
-Arguments prim_step {_} _ _.
+Global Arguments Sts {_} _.
+Global Arguments prim_step {_} _ _.
Notation states sts := (propset (state sts)).
Definition stsT_token := Empty_set.
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index 0584ed587..471583989 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -35,7 +35,7 @@ Section ofe.
Proof. intros ? v. induction v; apply _. Qed.
End ofe.
-Arguments vecO : clear implicits.
+Global Arguments vecO : clear implicits.
Typeclasses Opaque vec_dist.
Section proper.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 1c5fb7d2f..2b9b1224c 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -53,8 +53,8 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
view_rel_unit n :
∃ a, view_rel_holds n a ε
}.
-Arguments ViewRel {_ _} _ _.
-Arguments view_rel_holds {_ _} _ _ _ _.
+Global Arguments ViewRel {_ _} _ _.
+Global Arguments view_rel_holds {_ _} _ _ _ _.
Global Instance: Params (@view_rel_holds) 4 := {}.
Global Instance view_rel_ne {A B} (rel : view_rel A B) n :
@@ -77,9 +77,9 @@ always be constructed using [â—V] and [â—¯V], and never using the constructor
Record view {A B} (rel : nat → A → B → Prop) :=
View { view_auth_proj : option (frac * agree A) ; view_frag_proj : B }.
Add Printing Constructor view.
-Arguments View {_ _ _} _ _.
-Arguments view_auth_proj {_ _ _} _.
-Arguments view_frag_proj {_ _ _} _.
+Global Arguments View {_ _ _} _ _.
+Global Arguments view_auth_proj {_ _ _} _.
+Global Arguments view_frag_proj {_ _ _} _.
Global Instance: Params (@View) 3 := {}.
Global Instance: Params (@view_auth_proj) 3 := {}.
Global Instance: Params (@view_frag_proj) 3 := {}.
diff --git a/iris/base_logic/lib/auth.v b/iris/base_logic/lib/auth.v
index 6bed8f337..0df2a9fcf 100644
--- a/iris/base_logic/lib/auth.v
+++ b/iris/base_logic/lib/auth.v
@@ -209,4 +209,4 @@ Section auth.
Qed.
End auth.
-Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
+Global Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 533753fe8..33af48462 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -11,7 +11,7 @@ Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ
wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
-Arguments uPred_fupd {Σ _}.
+Global Arguments uPred_fupd {Σ _}.
Lemma uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index e79954711..60d5a7fd3 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -72,8 +72,8 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_name : gname;
gen_meta_name : gname
}.
-Arguments gen_heap_name {L V Σ _ _} _ : assert.
-Arguments gen_meta_name {L V Σ _ _} _ : assert.
+Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
+Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO V));
@@ -121,7 +121,7 @@ Section definitions.
Definition meta := meta_aux.(unseal).
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
-Arguments meta {L _ _ V Σ _ A _ _} l N x.
+Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index d340387fc..62ca46136 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -34,8 +34,8 @@ Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
inv_heap_name : gname
}.
-Arguments Inv_HeapG _ _ {_ _ _ _}.
-Arguments inv_heap_name {_ _ _ _ _} _ : assert.
+Global Arguments Inv_HeapG _ _ {_ _ _ _}.
+Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
@@ -75,7 +75,7 @@ Local Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
(* [inv_heap_inv] has no parameters to infer the types from, so we need to
make them explicit. *)
-Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
+Global Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
Global Instance: Params (@inv_mapsto_own) 8 := {}.
Global Instance: Params (@inv_mapsto) 7 := {}.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 0142e9c1c..6b23455dc 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -23,7 +23,7 @@ Definition ghost_var_def `{!ghost_varG Σ A} (γ : gname) (q : Qp) (a : A) : iPr
Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
Definition ghost_var := ghost_var_aux.(unseal).
Definition ghost_var_eq : @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
-Arguments ghost_var {Σ A _} γ q a.
+Global Arguments ghost_var {Σ A _} γ q a.
Local Ltac unseal := rewrite ?ghost_var_eq /ghost_var_def.
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 636f42c09..1144bf6f5 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -44,7 +44,7 @@ Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexi
Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
Definition gset_bij_own_auth_eq :
@gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
-Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
+Global Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
Definition gset_bij_own_elem_def `{gset_bijG Σ A B} (γ : gname)
(a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
@@ -52,7 +52,7 @@ Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexi
Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
Definition gset_bij_own_elem_eq :
@gset_bij_own_elem = @gset_bij_own_elem_def := seal_eq gset_bij_own_elem_aux.
-Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
+Global Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
Section gset_bij.
Context `{gset_bijG Σ A B}.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index 73f0cc7e1..e987fc3f2 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -11,7 +11,7 @@ Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
□ ∀ E, ⌜↑N ⊆ E⌠→ |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv := inv_aux.(unseal).
-Arguments inv {Σ _} N P.
+Global Arguments inv {Σ _} N P.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
Global Instance: Params (@inv) 3 := {}.
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 038a552ed..7c31a9c77 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -28,7 +28,7 @@ Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor;
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
-Arguments GFunctor _ {_}.
+Global Arguments GFunctor _ {_}.
Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 5c28871bd..ba3d1cef3 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -26,7 +26,7 @@ Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def). Proof. by eexi
Definition mono_nat_auth_own := mono_nat_auth_own_aux.(unseal).
Definition mono_nat_auth_own_eq :
@mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
-Arguments mono_nat_auth_own {Σ _} γ q n.
+Global Arguments mono_nat_auth_own {Σ _} γ q n.
Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mono_nat_lb n).
@@ -34,7 +34,7 @@ Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists.
Definition mono_nat_lb_own := mono_nat_lb_own_aux.(unseal).
Definition mono_nat_lb_own_eq :
@mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
-Arguments mono_nat_lb_own {Σ _} γ n.
+Global Arguments mono_nat_lb_own {Σ _} γ n.
Local Ltac unseal := rewrite
?mono_nat_auth_own_eq /mono_nat_auth_own_def
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 69d36e95a..de2d2e1f0 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -14,8 +14,8 @@ Class inG (Σ : gFunctors) (A : cmraT) := InG {
inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
inG_prf : A = inG_apply (iPropO Σ) _;
}.
-Arguments inG_id {_ _} _.
-Arguments inG_apply {_ _} _ _ {_}.
+Global Arguments inG_id {_ _} _.
+Global 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
@@ -72,7 +72,7 @@ Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Local Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
Definition own := own_aux.(unseal).
-Arguments own {Σ A _} γ a.
+Global Arguments own {Σ A _} γ a.
Local Definition own_eq : @own = @own_def := own_aux.(seal_eq).
Local Instance: Params (@own) 4 := {}.
@@ -288,15 +288,15 @@ Lemma own_update_3 γ a1 a2 a3 a' :
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
End global.
-Arguments own_valid {_ _} [_] _ _.
-Arguments own_valid_2 {_ _} [_] _ _ _.
-Arguments own_valid_3 {_ _} [_] _ _ _ _.
-Arguments own_valid_l {_ _} [_] _ _.
-Arguments own_valid_r {_ _} [_] _ _.
-Arguments own_updateP {_ _} [_] _ _ _ _.
-Arguments own_update {_ _} [_] _ _ _ _.
-Arguments own_update_2 {_ _} [_] _ _ _ _ _.
-Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
+Global Arguments own_valid {_ _} [_] _ _.
+Global Arguments own_valid_2 {_ _} [_] _ _ _.
+Global Arguments own_valid_3 {_ _} [_] _ _ _ _.
+Global Arguments own_valid_l {_ _} [_] _ _.
+Global Arguments own_valid_r {_ _} [_] _ _.
+Global Arguments own_updateP {_ _} [_] _ _ _ _.
+Global Arguments own_update {_ _} [_] _ _ _ _.
+Global Arguments own_update_2 {_ _} [_] _ _ _ _ _.
+Global Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{i : !inG Σ (A:ucmraT)} γ : ⊢ |==> own γ (ε:A).
Proof.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index d1a4b9bae..f28cce425 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -12,7 +12,7 @@ Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
proph_map_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V));
proph_map_name : gname
}.
-Arguments proph_map_name {_ _ _ _ _} _ : assert.
+Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
{ proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
diff --git a/iris/base_logic/lib/viewshifts.v b/iris/base_logic/lib/viewshifts.v
index e323b4d03..6dce54464 100644
--- a/iris/base_logic/lib/viewshifts.v
+++ b/iris/base_logic/lib/viewshifts.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
□ (P -∗ |={E1,E2}=> Q).
-Arguments vs {_ _} _ _ _%I _%I.
+Global Arguments vs {_ _} _ _ _%I _%I.
Global Instance: Params (@vs) 4 := {}.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 3c1d28ee6..5092971c7 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -37,7 +37,7 @@ Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
Next P.
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
-Arguments ownI {_ _} _ _%I.
+Global Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
Global Instance: Params (@invariant_unfold) 1 := {}.
Global Instance: Params (@ownI) 3 := {}.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 9eab3d8f4..9c4ca484c 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -111,7 +111,7 @@ Record uPred (M : ucmraT) : Type := UPred {
uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.
Bind Scope bi_scope with uPred.
-Arguments uPred_holds {_} _%I _ _ : simpl never.
+Global Arguments uPred_holds {_} _%I _ _ : simpl never.
Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 3 := {}.
@@ -154,7 +154,7 @@ Section cofe.
repeat intro. apply (chain_cauchy c _ i)=>//. by eapply uPred_mono.
Qed.
End cofe.
-Arguments uPredO : clear implicits.
+Global Arguments uPredO : clear implicits.
Global Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
@@ -253,7 +253,7 @@ Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
Solve Obligations with done.
Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
Definition uPred_pure := uPred_pure_aux.(unseal).
-Arguments uPred_pure {M}.
+Global Arguments uPred_pure {M}.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
@@ -262,7 +262,7 @@ Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
Definition uPred_and := uPred_and_aux.(unseal).
-Arguments uPred_and {M}.
+Global Arguments uPred_and {M}.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
@@ -270,7 +270,7 @@ Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
Definition uPred_or := uPred_or_aux.(unseal).
-Arguments uPred_or {M}.
+Global Arguments uPred_or {M}.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
@@ -283,7 +283,7 @@ Next Obligation.
Qed.
Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
Definition uPred_impl := uPred_impl_aux.(unseal).
-Arguments uPred_impl {M}.
+Global Arguments uPred_impl {M}.
Definition uPred_impl_eq :
@uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
@@ -292,7 +292,7 @@ Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
Definition uPred_forall := uPred_forall_aux.(unseal).
-Arguments uPred_forall {M A}.
+Global Arguments uPred_forall {M A}.
Definition uPred_forall_eq :
@uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
@@ -301,7 +301,7 @@ Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
Definition uPred_exist := uPred_exist_aux.(unseal).
-Arguments uPred_exist {M A}.
+Global Arguments uPred_exist {M A}.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
@@ -309,7 +309,7 @@ Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
Solve Obligations with naive_solver eauto 2 using dist_le.
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
-Arguments uPred_internal_eq {M A}.
+Global Arguments uPred_internal_eq {M A}.
Definition uPred_internal_eq_eq:
@uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
@@ -322,7 +322,7 @@ Next Obligation.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
Definition uPred_sep := uPred_sep_aux.(unseal).
-Arguments uPred_sep {M}.
+Global Arguments uPred_sep {M}.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
@@ -335,7 +335,7 @@ Next Obligation.
Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
Definition uPred_wand := uPred_wand_aux.(unseal).
-Arguments uPred_wand {M}.
+Global Arguments uPred_wand {M}.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
@@ -347,7 +347,7 @@ Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
Definition uPred_plainly := uPred_plainly_aux.(unseal).
-Arguments uPred_plainly {M}.
+Global Arguments uPred_plainly {M}.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
@@ -356,7 +356,7 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
-Arguments uPred_persistently {M}.
+Global Arguments uPred_persistently {M}.
Definition uPred_persistently_eq :
@uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
@@ -367,7 +367,7 @@ Next Obligation.
Qed.
Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
Definition uPred_later := uPred_later_aux.(unseal).
-Arguments uPred_later {M}.
+Global Arguments uPred_later {M}.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
@@ -379,7 +379,7 @@ Next Obligation.
Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
Definition uPred_ownM := uPred_ownM_aux.(unseal).
-Arguments uPred_ownM {M}.
+Global Arguments uPred_ownM {M}.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
@@ -388,7 +388,7 @@ Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
-Arguments uPred_cmra_valid {M A}.
+Global Arguments uPred_cmra_valid {M A}.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
@@ -404,7 +404,7 @@ Next Obligation.
Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
Definition uPred_bupd := uPred_bupd_aux.(unseal).
-Arguments uPred_bupd {M}.
+Global Arguments uPred_bupd {M}.
Definition uPred_bupd_eq :
@uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
@@ -428,7 +428,7 @@ Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
-Arguments uPred_holds {_} !_ _ _ /.
+Local Arguments uPred_holds {_} !_ _ _ /.
Local Hint Immediate uPred_in_entails : core.
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index e34dd8e45..357ef5d1d 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -44,7 +44,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
| _, _ => False
end%I.
Global Instance: Params (@big_sepL2) 3 := {}.
-Arguments big_sepL2 {PROP A B} _ !_ !_ /.
+Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
Typeclasses Opaque big_sepL2.
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
(big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
@@ -57,7 +57,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
[∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
Definition big_sepM2 := big_sepM2_aux.(unseal).
-Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
+Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
Global Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 9a10af530..0c8ac604a 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -3,31 +3,31 @@ From iris.bi Require Export interface.
From iris.prelude Require Import options.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
-Arguments bi_iff {_} _%I _%I : simpl never.
+Global Arguments bi_iff {_} _%I _%I : simpl never.
Global Instance: Params (@bi_iff) 1 := {}.
Infix "↔" := bi_iff : bi_scope.
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
((P -∗ Q) ∧ (Q -∗ P))%I.
-Arguments bi_wand_iff {_} _%I _%I : simpl never.
+Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
Global Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
-Arguments Persistent {_} _%I : simpl never.
-Arguments persistent {_} _%I {_}.
+Global Arguments Persistent {_} _%I : simpl never.
+Global Arguments persistent {_} _%I {_}.
Global Hint Mode Persistent + ! : typeclass_instances.
Global Instance: Params (@Persistent) 1 := {}.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
-Arguments bi_affinely {_} _%I : simpl never.
+Global Arguments bi_affinely {_} _%I : simpl never.
Global Instance: Params (@bi_affinely) 1 := {}.
Typeclasses Opaque bi_affinely.
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 {_}.
+Global Arguments Affine {_} _%I : simpl never.
+Global Arguments affine {_} _%I {_}.
Global Hint Mode Affine + ! : typeclass_instances.
Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
@@ -39,47 +39,47 @@ Class BiPositive (PROP : bi) :=
Global Hint Mode BiPositive ! : typeclass_instances.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
-Arguments bi_absorbingly {_} _%I : simpl never.
+Global Arguments bi_absorbingly {_} _%I : simpl never.
Global Instance: Params (@bi_absorbingly) 1 := {}.
Typeclasses Opaque bi_absorbingly.
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.
+Global Arguments Absorbing {_} _%I : simpl never.
+Global Arguments absorbing {_} _%I.
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.
-Arguments bi_persistently_if {_} !_ _%I /.
+Global Arguments bi_persistently_if {_} !_ _%I /.
Global Instance: Params (@bi_persistently_if) 2 := {}.
Typeclasses Opaque bi_persistently_if.
Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <affine> P else P)%I.
-Arguments bi_affinely_if {_} !_ _%I /.
+Global Arguments bi_affinely_if {_} !_ _%I /.
Global Instance: Params (@bi_affinely_if) 2 := {}.
Typeclasses Opaque bi_affinely_if.
Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <absorb> P else P)%I.
-Arguments bi_absorbingly_if {_} !_ _%I /.
+Global Arguments bi_absorbingly_if {_} !_ _%I /.
Global Instance: Params (@bi_absorbingly_if) 2 := {}.
Typeclasses Opaque bi_absorbingly_if.
Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affine> <pers> P)%I.
-Arguments bi_intuitionistically {_} _%I : simpl never.
+Global Arguments bi_intuitionistically {_} _%I : simpl never.
Global Instance: Params (@bi_intuitionistically) 1 := {}.
Typeclasses Opaque bi_intuitionistically.
Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then â–¡ P else P)%I.
-Arguments bi_intuitionistically_if {_} !_ _%I /.
+Global Arguments bi_intuitionistically_if {_} !_ _%I /.
Global Instance: Params (@bi_intuitionistically_if) 2 := {}.
Typeclasses Opaque bi_intuitionistically_if.
Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
@@ -90,19 +90,19 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
| S n' => â–· â–·^n' P
end%I
where "â–·^ n P" := (bi_laterN n P) : bi_scope.
-Arguments bi_laterN {_} !_%nat_scope _%I.
+Global Arguments bi_laterN {_} !_%nat_scope _%I.
Global Instance: Params (@bi_laterN) 2 := {}.
Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
-Arguments bi_except_0 {_} _%I : simpl never.
+Global Arguments bi_except_0 {_} _%I : simpl never.
Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
Global Instance: Params (@bi_except_0) 1 := {}.
Typeclasses Opaque bi_except_0.
Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
-Arguments Timeless {_} _%I : simpl never.
-Arguments timeless {_} _%I {_}.
+Global Arguments Timeless {_} _%I : simpl never.
+Global Arguments timeless {_} _%I {_}.
Global Hint Mode Timeless + ! : typeclass_instances.
Global Instance: Params (@Timeless) 1 := {}.
@@ -114,7 +114,7 @@ Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
| None => Q
| Some P => (P -∗ Q)%I
end.
-Arguments bi_wandM {_} !_%I _%I /.
+Global Arguments bi_wandM {_} !_%I _%I /.
Notation "mP -∗? Q" := (bi_wandM mP Q)
(at level 99, Q at level 200, right associativity) : bi_scope.
@@ -129,7 +129,7 @@ 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).
Global Hint Mode BiLöb ! : typeclass_instances.
-Arguments löb_weak {_ _} _ _.
+Global Arguments löb_weak {_ _} _ _.
Notation BiLaterContractive PROP :=
(Contractive (bi_later (PROP:=PROP))) (only parsing).
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 8bcfde62e..fa2c800a7 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
Set Default Proof Using "Type*".
Class Embed (A B : Type) := embed : A → B.
-Arguments embed {_ _ _} _%I : simpl never.
+Global Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
Global Instance: Params (@embed) 3 := {}.
Typeclasses Opaque embed.
@@ -49,7 +49,7 @@ Class BiEmbed (PROP1 PROP2 : bi) := {
}.
Global Hint Mode BiEmbed ! - : typeclass_instances.
Global Hint Mode BiEmbed - ! : typeclass_instances.
-Arguments bi_embed_embed : simpl never.
+Global Arguments bi_embed_embed : simpl never.
Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 3539069a1..3638fa926 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -201,21 +201,21 @@ Global Instance: Params (@bi_wand) 1 := {}.
Global Instance: Params (@bi_persistently) 1 := {}.
Global Instance: Params (@bi_later) 1 := {}.
-Arguments bi_car : simpl never.
-Arguments bi_dist : simpl never.
-Arguments bi_equiv : simpl never.
-Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
-Arguments bi_emp {PROP} : simpl never, rename.
-Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
-Arguments bi_and {PROP} _%I _%I : simpl never, rename.
-Arguments bi_or {PROP} _%I _%I : simpl never, rename.
-Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
-Arguments bi_forall {PROP _} _%I : simpl never, rename.
-Arguments bi_exist {PROP _} _%I : simpl never, rename.
-Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
-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.
+Global Arguments bi_car : simpl never.
+Global Arguments bi_dist : simpl never.
+Global Arguments bi_equiv : simpl never.
+Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_emp {PROP} : simpl never, rename.
+Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
+Global Arguments bi_and {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_or {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
+Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
+Global Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_persistently {PROP} _%I : simpl never, rename.
+Global Arguments bi_later {PROP} _%I : simpl never, rename.
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
@@ -258,7 +258,7 @@ Notation "â–· P" := (bi_later P) : bi_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
-Arguments bi_emp_valid {_} _%I : simpl never.
+Global Arguments bi_emp_valid {_} _%I : simpl never.
Typeclasses Opaque bi_emp_valid.
Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 6e78aed8b..da7d84cfd 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -8,7 +8,7 @@ can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
Class InternalEq (PROP : bi) :=
internal_eq : ∀ {A : ofeT}, A → A → PROP.
-Arguments internal_eq {_ _ _} _ _ : simpl never.
+Global Arguments internal_eq {_ _ _} _ _ : simpl never.
Global Hint Mode InternalEq ! : typeclass_instances.
Global Instance: Params (@internal_eq) 3 := {}.
Infix "≡" := internal_eq : bi_scope.
@@ -41,7 +41,7 @@ Class BiInternalEq (PROP : bi) := {
bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
}.
Global Hint Mode BiInternalEq ! : typeclass_instances.
-Arguments bi_internal_eq_internal_eq : simpl never.
+Global Arguments bi_internal_eq_internal_eq : simpl never.
Section internal_eq_laws.
Context `{BiInternalEq PROP}.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index a7272ddc2..731e88dc2 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -89,11 +89,11 @@ End definition.
(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
Definition atomic_update := atomic_update_aux.(unseal).
-Arguments atomic_update {PROP _ TA TB}.
+Global Arguments atomic_update {PROP _ TA TB}.
Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
-Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
-Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
+Global Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
+Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
(** Notation: Atomic updates *)
Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 592c2aff4..156759a0d 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -120,7 +120,7 @@ Module inv. Section inv.
(** We have the update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
Context (fupd : mask → PROP → PROP).
- Arguments fupd _ _%I.
+ Global Arguments fupd _ _%I.
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
@@ -129,7 +129,7 @@ Module inv. Section inv.
(** We have invariants *)
Context (name : Type) (inv : name → PROP → PROP).
- Arguments inv _ _%I.
+ Global Arguments inv _ _%I.
Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
Hypothesis inv_fupd :
@@ -287,7 +287,7 @@ Module linear. Section linear.
(** We have the mask-changing update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
Context (fupd : mask → mask → PROP → PROP).
- Arguments fupd _ _ _%I.
+ Global Arguments fupd _ _ _%I.
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 9ca541ab8..64a5fc7d7 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -9,18 +9,18 @@ Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
-Arguments bi_mono_pred {_ _ _ _} _ _.
+Global Arguments bi_mono_pred {_ _ _ _} _ _.
Local Existing Instance bi_mono_pred_ne.
Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
-Arguments bi_least_fixpoint : simpl never.
+Global Arguments bi_least_fixpoint : simpl never.
Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
-Arguments bi_greatest_fixpoint : simpl never.
+Global Arguments bi_greatest_fixpoint : simpl never.
Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 68eb9228f..e7c88ae53 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -4,15 +4,15 @@ From iris.prelude Require Import options.
Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
-Arguments Fractional {_} _%I : simpl never.
+Global Arguments Fractional {_} _%I : simpl never.
Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
as_fractional : P ⊣⊢ Φ q;
as_fractional_fractional :> Fractional Φ
}.
-Arguments AsFractional {_} _%I _%I _%Qp.
+Global Arguments AsFractional {_} _%I _%I _%Qp.
-Arguments fractional {_ _ _} _ _.
+Global Arguments fractional {_ _ _} _ _.
Global Hint Mode AsFractional - + - - : typeclass_instances.
(* To make [as_fractional_fractional] a useful instance, we have to
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 7c21a1e4b..0ab92ec48 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -5,8 +5,8 @@ From iris.prelude Require Import options.
(** The class of laterable assertions *)
Class Laterable {PROP : bi} (P : PROP) := laterable :
P -∗ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
-Arguments Laterable {_} _%I : simpl never.
-Arguments laterable {_} _%I {_}.
+Global Arguments Laterable {_} _%I : simpl never.
+Global Arguments laterable {_} _%I {_}.
Global Hint Mode Laterable + ! : typeclass_instances.
Section instances.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index b0ebb3f2e..68189d8fd 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -106,10 +106,10 @@ Global Instance monPred_at_proper (R : relation I) :
Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
End Ofe_Cofe.
-Arguments monPred _ _ : clear implicits.
-Arguments monPred_at {_ _} _%I _.
+Global Arguments monPred _ _ : clear implicits.
+Global Arguments monPred_at {_ _} _%I _.
Local Existing Instance monPred_mono.
-Arguments monPredO _ _ : clear implicits.
+Global Arguments monPredO _ _ : clear implicits.
(** BI canonical structure *)
@@ -220,8 +220,8 @@ Definition monPred_later := monPred_later_aux.(unseal).
Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
End Bi.
-Arguments monPred_objectively {_ _} _%I.
-Arguments monPred_subjectively {_ _} _%I.
+Global Arguments monPred_objectively {_ _} _%I.
+Global Arguments monPred_subjectively {_ _} _%I.
Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
@@ -321,8 +321,8 @@ End canonical.
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 {_}.
+Global Arguments Objective {_ _} _%I.
+Global Arguments objective_at {_ _} _%I {_}.
Global Hint Mode Objective + + ! : typeclass_instances.
Global Instance: Params (@Objective) 2 := {}.
@@ -765,7 +765,7 @@ Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
-Arguments monPred_bupd {_}.
+Local Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
@@ -831,7 +831,7 @@ Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) :
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
Proof. by eexists. Qed.
Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
-Arguments monPred_internal_eq {_}.
+Local Arguments monPred_internal_eq {_}.
Lemma monPred_internal_eq_eq `{!BiInternalEq PROP} :
@internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
@@ -886,7 +886,7 @@ Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
Next Obligation. solve_proper. Qed.
Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
Definition monPred_fupd := monPred_fupd_aux.(unseal).
-Arguments monPred_fupd {_}.
+Local Arguments monPred_fupd {_}.
Lemma monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
@@ -924,7 +924,7 @@ Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
MonPred (λ _, ∀ i, ■(P i))%I _.
Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
Definition monPred_plainly := monPred_plainly_aux.(unseal).
-Arguments monPred_plainly {_}.
+Local Arguments monPred_plainly {_}.
Lemma monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index cd52e2ae3..5549afda8 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -7,7 +7,7 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
Set Default Proof Using "Type*".
Class Plainly (A : Type) := plainly : A → A.
-Arguments plainly {A}%type_scope {_} _%I.
+Global Arguments plainly {A}%type_scope {_} _%I.
Global Hint Mode Plainly ! : typeclass_instances.
Global Instance: Params (@plainly) 2 := {}.
Notation "â– P" := (plainly P) : bi_scope.
@@ -43,21 +43,21 @@ Class BiPlainly (PROP : bi) := {
bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
}.
Global Hint Mode BiPlainly ! : typeclass_instances.
-Arguments bi_plainly_plainly : simpl never.
+Global Arguments bi_plainly_plainly : simpl never.
Class BiPlainlyExist `{!BiPlainly PROP} :=
plainly_exist_1 A (Ψ : A → PROP) :
■(∃ a, Ψ a) ⊢ ∃ a, ■(Ψ a).
-Arguments BiPlainlyExist : clear implicits.
-Arguments BiPlainlyExist _ {_}.
-Arguments plainly_exist_1 _ {_ _} _.
+Global Arguments BiPlainlyExist : clear implicits.
+Global Arguments BiPlainlyExist _ {_}.
+Global Arguments plainly_exist_1 _ {_ _} _.
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 _ {_ _ _} _.
+Global Arguments BiPropExt : clear implicits.
+Global Arguments BiPropExt _ {_ _}.
+Global Arguments prop_ext_2 _ {_ _ _} _.
Global Hint Mode BiPropExt ! - - : typeclass_instances.
Section plainly_laws.
@@ -92,14 +92,14 @@ End plainly_laws.
(* Derived properties and connectives *)
Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■P.
-Arguments Plain {_ _} _%I : simpl never.
-Arguments plain {_ _} _%I {_}.
+Global Arguments Plain {_ _} _%I : simpl never.
+Global Arguments plain {_ _} _%I {_}.
Global Hint Mode Plain + - ! : typeclass_instances.
Global Instance: Params (@Plain) 1 := {}.
Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
(if p then â– P else P)%I.
-Arguments plainly_if {_ _} !_ _%I /.
+Global Arguments plainly_if {_ _} !_ _%I /.
Global Instance: Params (@plainly_if) 2 := {}.
Typeclasses Opaque plainly_if.
diff --git a/iris/bi/telescopes.v b/iris/bi/telescopes.v
index b2836192c..66bde8307 100644
--- a/iris/bi/telescopes.v
+++ b/iris/bi/telescopes.v
@@ -8,10 +8,10 @@ Import bi.
(** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
-Arguments bi_texist {_ !_} _ /.
+Global Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
-Arguments bi_tforall {_ !_} _ /.
+Global Arguments bi_tforall {_ !_} _ /.
Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
(at level 200, x binder, y binder, right associativity,
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 5d797983f..8ef588bb5 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -11,7 +11,7 @@ bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
Global Instance : Params (@bupd) 2 := {}.
Global Hint Mode BUpd ! : typeclass_instances.
-Arguments bupd {_}%type_scope {_} _%bi_scope.
+Global Arguments bupd {_}%type_scope {_} _%bi_scope.
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
@@ -20,7 +20,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
Global Instance: Params (@fupd) 4 := {}.
Global Hint Mode FUpd ! : typeclass_instances.
-Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
+Global Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
@@ -83,14 +83,14 @@ Class BiBUpd (PROP : bi) := {
bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.
Global Hint Mode BiBUpd ! : typeclass_instances.
-Arguments bi_bupd_bupd : simpl never.
+Global Arguments bi_bupd_bupd : simpl never.
Class BiFUpd (PROP : bi) := {
bi_fupd_fupd :> FUpd PROP;
bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
Global Hint Mode BiFUpd ! : typeclass_instances.
-Arguments bi_fupd_fupd : simpl never.
+Global Arguments bi_fupd_fupd : simpl never.
Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index 5a8d42aec..3bcc9cfe9 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -30,12 +30,12 @@ different [A], the plan is to generalize the notation to use [Inhabited] instead
to pick a default value depending on [A]. *)
Class Wp (Λ : language) (PROP A : Type) :=
wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Arguments wp {_ _ _ _} _ _ _%E _%I.
+Global Arguments wp {_ _ _ _} _ _ _%E _%I.
Global Instance: Params (@wp) 7 := {}.
Class Twp (Λ : language) (PROP A : Type) :=
twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Arguments twp {_ _ _ _} _ _ _%E _%I.
+Global Arguments twp {_ _ _ _} _ _ _%E _%I.
Global Instance: Params (@twp) 7 := {}.
(** Notations for partial weakest preconditions *)
diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index 09725d72c..a4c2e0c07 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -72,13 +72,13 @@ Structure ectxLanguage := EctxLanguage {
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
-Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
-Arguments of_val {_} _.
-Arguments to_val {_} _.
-Arguments empty_ectx {_}.
-Arguments comp_ectx {_} _ _.
-Arguments fill {_} _ _.
-Arguments head_step {_} _ _ _ _ _ _.
+Global Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
+Global Arguments of_val {_} _.
+Global Arguments to_val {_} _.
+Global Arguments empty_ectx {_}.
+Global Arguments comp_ectx {_} _ _.
+Global Arguments fill {_} _ _.
+Global Arguments head_step {_} _ _ _ _ _ _.
(* From an ectx_language, we can construct a language. *)
Section ectx_language.
@@ -309,7 +309,7 @@ Section ectx_language.
Proof. apply: pure_exec_ctx. Qed.
End ectx_language.
-Arguments ectx_lang : clear implicits.
+Global Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.
(* This definition makes sure that the fields of the [language] record do not
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index bbb6d9052..55dc11ff8 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -76,11 +76,11 @@ Structure ectxiLanguage := EctxiLanguage {
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
-Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
-Arguments of_val {_} _.
-Arguments to_val {_} _.
-Arguments fill_item {_} _ _.
-Arguments head_step {_} _ _ _ _ _ _.
+Global Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
+Global Arguments of_val {_} _.
+Global Arguments to_val {_} _.
+Global Arguments fill_item {_} _ _.
+Global Arguments head_step {_} _ _ _ _ _ _.
Section ectxi_language.
Context {Λ : ectxiLanguage}.
@@ -155,8 +155,8 @@ Section ectxi_language.
Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
End ectxi_language.
-Arguments ectxi_lang_ectx : clear implicits.
-Arguments ectxi_lang : clear implicits.
+Global Arguments ectxi_lang_ectx : clear implicits.
+Global Arguments ectxi_lang : clear implicits.
Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
Coercion ectxi_lang : ectxiLanguage >-> language.
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index b15008931..98f3e685f 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -36,10 +36,10 @@ Declare Scope val_scope.
Delimit Scope val_scope with V.
Bind Scope val_scope with val.
-Arguments Language {_ _ _ _ _ _ _} _.
-Arguments of_val {_} _.
-Arguments to_val {_} _.
-Arguments prim_step {_} _ _ _ _ _ _.
+Global Arguments Language {_ _ _ _ _ _ _} _.
+Global Arguments of_val {_} _.
+Global Arguments to_val {_} _.
+Global Arguments prim_step {_} _ _ _ _ _ _.
Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 469d88387..5dadf421f 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -61,7 +61,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
:= λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
Definition twp' := twp_aux.(unseal).
-Arguments twp' {Λ Σ _}.
+Global Arguments twp' {Λ Σ _}.
Existing Instance twp'.
Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
Proof. rewrite -twp_aux.(seal_eq) //. Qed.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 1123c57fa..c10cd66f5 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -48,7 +48,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
λ s : stuckness, fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
Definition wp' := wp_aux.(unseal).
-Arguments wp' {Λ Σ _}.
+Global Arguments wp' {Λ Σ _}.
Existing Instance wp'.
Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 20a98f6bb..f782aeb3e 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -104,15 +104,15 @@ Fixpoint pm_app {A} (l1 l2 : list A) : list A :=
Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
match mx with Some x => f x | None => None end.
-Arguments pm_option_bind {_ _} _ !_ /.
+Global Arguments pm_option_bind {_ _} _ !_ /.
Definition pm_from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end.
-Arguments pm_from_option {_ _} _ _ !_ /.
+Global Arguments pm_from_option {_ _} _ _ !_ /.
Definition pm_option_fun {A B} (f : option (A → B)) (x : A) : option B :=
match f with None => None | Some f => Some (f x) end.
-Arguments pm_option_fun {_ _} !_ _ /.
+Global Arguments pm_option_fun {_ _} !_ _ /.
(* Can't write [id] here as that would not reduce. *)
Notation pm_default := (pm_from_option (λ x, x)).
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index a532207d2..dd4c2a2c6 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -7,26 +7,26 @@ Import bi.
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 {_}.
+Global Arguments FromAssumption {_} _ _%I _%I : simpl never.
+Global Arguments from_assumption {_} _ _%I _%I {_}.
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 {_}.
+Global Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
+Global Arguments knownl_from_assumption {_} _ _%I _%I {_}.
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 {_}.
+Global Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
+Global Arguments knownr_from_assumption {_} _ _%I _%I {_}.
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 {_}.
+Global Arguments IntoPure {_} _%I _%type_scope : simpl never.
+Global Arguments into_pure {_} _%I _%type_scope {_}.
Global Hint Mode IntoPure + ! - : typeclass_instances.
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
@@ -67,8 +67,8 @@ Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
there we can just ask that [P] is [Affine]. *)
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 {_}.
+Global Arguments FromPure {_} _ _%I _%type_scope : simpl never.
+Global Arguments from_pure {_} _ _%I _%type_scope {_}.
Global Hint Mode FromPure + - ! - : typeclass_instances.
Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
@@ -81,14 +81,14 @@ Global Hint Extern 0 (FromPureT _ _ _) =>
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 {_}.
+Global Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
+Global Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
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 {_}.
+Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
+Global Arguments into_persistent {_} _ _%I _%I {_}.
Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
@@ -110,8 +110,8 @@ modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
Class FromModal {PROP1 PROP2 : bi} {A}
(M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
from_modal : M Q ⊢ P.
-Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
-Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
+Global Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
+Global Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
Global Hint Mode FromModal - + - - - ! - : typeclass_instances.
(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
@@ -120,8 +120,8 @@ proposition [Q].
The input is [Q] and the output is [P]. *)
Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : <affine> Q ⊢ P.
-Arguments FromAffinely {_} _%I _%I : simpl never.
-Arguments from_affinely {_} _%I _%I {_}.
+Global Arguments FromAffinely {_} _%I _%I : simpl never.
+Global Arguments from_affinely {_} _%I _%I {_}.
Global Hint Mode FromAffinely + - ! : typeclass_instances.
(** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
@@ -130,8 +130,8 @@ the proposition [Q].
The input is [Q] and the output is [P]. *)
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
into_absorbingly : P ⊢ <absorb> Q.
-Arguments IntoAbsorbingly {_} _%I _%I.
-Arguments into_absorbingly {_} _%I _%I {_}.
+Global Arguments IntoAbsorbingly {_} _%I _%I.
+Global Arguments into_absorbingly {_} _%I _%I {_}.
Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
(** Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
@@ -144,87 +144,87 @@ Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
- Instantiate the premise of the wand or implication. *)
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 {_}.
+Global Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
+Global Arguments into_wand {_} _ _ _%I _%I _%I {_}.
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.
+Global Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
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 {_}.
+Global Arguments FromWand {_} _%I _%I _%I : simpl never.
+Global Arguments from_wand {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments FromImpl {_} _%I _%I _%I : simpl never.
+Global Arguments from_impl {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments FromSep {_} _%I _%I _%I : simpl never.
+Global Arguments from_sep {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments FromAnd {_} _%I _%I _%I : simpl never.
+Global Arguments from_and {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
+Global Arguments into_and {_} _ _%I _%I _%I {_}.
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 {_}.
+Global Arguments IntoSep {_} _%I _%I _%I : simpl never.
+Global Arguments into_sep {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments FromOr {_} _%I _%I _%I : simpl never.
+Global Arguments from_or {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments IntoOr {_} _%I _%I _%I : simpl never.
+Global Arguments into_or {_} _%I _%I _%I {_}.
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 {_}.
+Global Arguments FromExist {_ _} _%I _%I : simpl never.
+Global Arguments from_exist {_ _} _%I _%I {_}.
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 _ {_}.
+Global Arguments IntoExist {_ _} _%I _%I _ : simpl never.
+Global Arguments into_exist {_ _} _%I _%I _ {_}.
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 {_}.
+Global Arguments IntoForall {_ _} _%I _%I : simpl never.
+Global Arguments into_forall {_ _} _%I _%I {_}.
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 _ {_}.
+Global Arguments FromForall {_ _} _%I _%I _ : simpl never.
+Global Arguments from_forall {_ _} _%I _%I _ {_}.
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 {_}.
+Global Arguments IsExcept0 {_} _%I : simpl never.
+Global Arguments is_except_0 {_} _%I {_}.
Global Hint Mode IsExcept0 + ! : typeclass_instances.
(** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
@@ -248,16 +248,16 @@ originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
modality, would have a side-condition [φ] on the masks. *)
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 {_}.
+Global Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
+Global Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
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. *)
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 {_}.
+Global Arguments AddModal {_} _%I _%I _%I : simpl never.
+Global Arguments add_modal {_} _%I _%I _%I {_}.
Global Hint Mode AddModal + - ! ! : typeclass_instances.
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
@@ -277,8 +277,8 @@ Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
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 {_}.
+Global Arguments Frame {_} _ _%I _%I _%I.
+Global Arguments frame {_} _ _%I _%I _%I {_}.
Global Hint Mode Frame + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed.
@@ -286,8 +286,8 @@ If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
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 _ {_}.
+Global Arguments MaybeFrame {_} _ _%I _%I _%I _.
+Global Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
Global Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
@@ -312,105 +312,105 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
Mode to disable all the instances that would have this behavior. *)
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
-Arguments MakeEmbed {_ _ _} _%I _%I.
+Global Arguments MakeEmbed {_ _ _} _%I _%I.
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.
+Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
-Arguments MakeSep {_} _%I _%I _%I.
+Global Arguments MakeSep {_} _%I _%I _%I.
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.
+Global Arguments KnownLMakeSep {_} _%I _%I _%I.
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.
+Global Arguments KnownRMakeSep {_} _%I _%I _%I.
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.
+Global Arguments MakeAnd {_} _%I _%I _%I.
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.
+Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
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.
+Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
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.
+Global Arguments MakeOr {_} _%I _%I _%I.
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.
+Global Arguments KnownLMakeOr {_} _%I _%I _%I.
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.
+Global Arguments KnownRMakeOr {_} _%I _%I _%I.
Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
-Arguments MakeAffinely {_} _%I _%I.
+Global Arguments MakeAffinely {_} _%I _%I.
Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
known_make_affinely :> MakeAffinely P Q.
-Arguments KnownMakeAffinely {_} _%I _%I.
+Global Arguments KnownMakeAffinely {_} _%I _%I.
Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
-Arguments MakeIntuitionistically {_} _%I _%I.
+Global Arguments MakeIntuitionistically {_} _%I _%I.
Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
known_make_intuitionistically :> MakeIntuitionistically P Q.
-Arguments KnownMakeIntuitionistically {_} _%I _%I.
+Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
-Arguments MakeAbsorbingly {_} _%I _%I.
+Global Arguments MakeAbsorbingly {_} _%I _%I.
Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
known_make_absorbingly :> MakeAbsorbingly P Q.
-Arguments KnownMakeAbsorbingly {_} _%I _%I.
+Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
-Arguments MakePersistently {_} _%I _%I.
+Global Arguments MakePersistently {_} _%I _%I.
Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
known_make_persistently :> MakePersistently P Q.
-Arguments KnownMakePersistently {_} _%I _%I.
+Global Arguments KnownMakePersistently {_} _%I _%I.
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.
+Global Arguments MakeLaterN {_} _%nat _%I _%I.
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.
+Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
-Arguments MakeExcept0 {_} _%I _%I.
+Global Arguments MakeExcept0 {_} _%I _%I.
Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
-Arguments KnownMakeExcept0 {_} _%I _%I.
+Global Arguments KnownMakeExcept0 {_} _%I _%I.
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 {_}.
+Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
+Global Arguments into_except_0 {_} _%I _%I {_}.
Global Hint Mode IntoExcept0 + ! - : typeclass_instances.
Global Hint Mode IntoExcept0 + - ! : typeclass_instances.
@@ -450,13 +450,13 @@ Proof. iIntros "H". iFrame "H". Qed.
*)
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 {_}.
+Global Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
+Global Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
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.
+Global Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Global Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
@@ -475,8 +475,8 @@ embeddings using [iModIntro].
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
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 {_}.
+Global Arguments IntoEmbed {_ _ _} _%I _%I.
+Global Arguments into_embed {_ _ _} _%I _%I {_}.
Global Hint Mode IntoEmbed + + + ! - : typeclass_instances.
(* We use two type classes for [AsEmpValid], in order to avoid loops in
@@ -493,10 +493,10 @@ Global Hint Mode IntoEmbed + + + ! - : typeclass_instances.
projections for hints modes would make this fail.*)
Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid : φ ↔ ⊢ P.
-Arguments AsEmpValid {_} _%type _%I.
+Global Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_0 : AsEmpValid φ P.
-Arguments AsEmpValid0 {_} _%type _%I.
+Global Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
@@ -509,7 +509,7 @@ Proof. by apply as_emp_valid. Qed.
(* Input: [P]; Outputs: [N],
Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
-Arguments IntoInv {_} _%I _.
+Global Arguments IntoInv {_} _%I _.
Global Hint Mode IntoInv + ! - : typeclass_instances.
(** Accessors.
@@ -532,8 +532,8 @@ Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
(α β : X → PROP) (mγ : X → option PROP)
(Q : PROP) (Q' : X → 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 {_}.
+Global Arguments ElimAcc {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Global Arguments elim_acc {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
(* Turn [P] into an accessor.
@@ -549,8 +549,8 @@ Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
(M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option 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.
+Global Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
+Global Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
(* The typeclass used for the [iInv] tactic.
@@ -577,8 +577,8 @@ Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
(Q : PROP) (Q' : X → 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 {_}.
+Global Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Global Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
(** We make sure that tactics that perform actions on *specific* hypotheses or
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 2a8f370a4..ef474074a 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -575,8 +575,8 @@ Qed.
(** * Combining *)
Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
from_seps : [∗] Qs ⊢ P.
-Arguments FromSeps {_} _%I _%I.
-Arguments from_seps {_} _%I _%I {_}.
+Local Arguments FromSeps {_} _%I _%I.
+Local Arguments from_seps {_} _%I _%I {_}.
Global Instance from_seps_nil : @FromSeps PROP emp [].
Proof. by rewrite /FromSeps. Qed.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index be3fdbe4f..ba5796dd3 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -7,8 +7,8 @@ Import bi.
Inductive env (A : Type) : Type :=
| Enil : env A
| Esnoc : env A → ident → A → env A.
-Arguments Enil {_}.
-Arguments Esnoc {_} _ _ _.
+Global Arguments Enil {_}.
+Global Arguments Esnoc {_} _ _ _.
Global Instance: Params (@Enil) 1 := {}.
Global Instance: Params (@Esnoc) 1 := {}.
@@ -216,10 +216,10 @@ Record envs (PROP : bi) := Envs {
env_counter : positive (** A counter to generate fresh hypothesis names *)
}.
Add Printing Constructor envs.
-Arguments Envs {_} _ _ _.
-Arguments env_intuitionistic {_} _.
-Arguments env_spatial {_} _.
-Arguments env_counter {_} _.
+Global Arguments Envs {_} _ _ _.
+Global Arguments env_intuitionistic {_} _.
+Global Arguments env_spatial {_} _.
+Global Arguments env_counter {_} _.
(** We now define the judgment [envs_entails Δ Q] for proof mode entailments.
This judgment expresses that [Q] can be proved under the proof mode environment
@@ -254,7 +254,7 @@ Global Instance: Params (@of_envs') 1 := {}.
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
of_envs' (env_intuitionistic Δ) (env_spatial Δ).
Global Instance: Params (@of_envs) 1 := {}.
-Arguments of_envs : simpl never.
+Global Arguments of_envs : simpl never.
Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
of_envs' Γp Γs ⊢ Q.
@@ -268,7 +268,7 @@ Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
Definition envs_entails_eq :
@envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
-Arguments envs_entails {PROP} Δ Q%I.
+Global Arguments envs_entails {PROP} Δ Q%I.
Global Instance: Params (@envs_entails) 1 := {}.
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
diff --git a/iris/proofmode/ident_name.v b/iris/proofmode/ident_name.v
index 2457b844f..a254743fb 100644
--- a/iris/proofmode/ident_name.v
+++ b/iris/proofmode/ident_name.v
@@ -24,7 +24,7 @@ Notation to_ident_name id := (λ id:unit, id) (only parsing).
to an identifier rather than a lambda; for example, if the user writes
[bi_exist Φ], there is no binder anywhere to extract. *)
Class AsIdentName {A B} (f : A → B) (name : ident_name) := as_ident_name {}.
-Arguments as_ident_name {A B f} name : assert.
+Global Arguments as_ident_name {A B f} name : assert.
Ltac solve_as_ident_name :=
lazymatch goal with
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index a600e6e0b..e3643a759 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -740,7 +740,7 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
(** * The specialize and pose proof tactics *)
Record iTrm {X As S} :=
ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
-Arguments ITrm {_ _ _} _ _ _.
+Global Arguments ITrm {_ _ _} _ _ _.
Notation "( H $! x1 .. xn )" :=
(ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index 1e65317da..f1255cdc7 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -55,11 +55,11 @@ Inductive modality_action (PROP1 : bi) : bi → Type :=
| MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
| MIEnvClear {PROP2} : modality_action PROP1 PROP2
| MIEnvId : modality_action PROP1 PROP1.
-Arguments MIEnvIsEmpty {_ _}.
-Arguments MIEnvForall {_} _.
-Arguments MIEnvTransform {_ _} _.
-Arguments MIEnvClear {_ _}.
-Arguments MIEnvId {_}.
+Global Arguments MIEnvIsEmpty {_ _}.
+Global Arguments MIEnvForall {_} _.
+Global Arguments MIEnvTransform {_ _} _.
+Global Arguments MIEnvClear {_ _}.
+Global Arguments MIEnvId {_}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
@@ -105,9 +105,9 @@ Record modality (PROP1 PROP2 : bi) := Modality {
modality_mixin_of :
modality_mixin modality_car modality_intuitionistic_action modality_spatial_action
}.
-Arguments Modality {_ _} _ {_ _} _.
-Arguments modality_intuitionistic_action {_ _} _.
-Arguments modality_spatial_action {_ _} _.
+Global Arguments Modality {_ _} _ {_ _} _.
+Global Arguments modality_intuitionistic_action {_ _} _.
+Global Arguments modality_spatial_action {_ _} _.
Section modality.
Context {PROP1 PROP2} (M : modality PROP1 PROP2).
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index ce13a62d0..580854139 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (ð“Ÿ : PROP) :=
make_monPred_at : P i ⊣⊢ ð“Ÿ.
-Arguments MakeMonPredAt {_ _} _ _%I _%I.
+Global 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. *)
@@ -24,7 +24,7 @@ Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
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.
+Global Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
Global Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
Section modalities.
diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index 0f4fd26c0..0521f8a7e 100644
--- a/iris/proofmode/notation.v
+++ b/iris/proofmode/notation.v
@@ -4,9 +4,9 @@ From iris.prelude Require Import options.
Declare Scope proof_scope.
Delimit Scope proof_scope with env.
-Arguments Envs _ _%proof_scope _%proof_scope _.
-Arguments Enil {_}.
-Arguments Esnoc {_} _%proof_scope _%string _%I.
+Global Arguments Envs _ _%proof_scope _%proof_scope _.
+Global Arguments Enil {_}.
+Global Arguments Esnoc {_} _%proof_scope _%string _%I.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ (INamed H) P%I)
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index ef804c4f8..5fc399342 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -9,7 +9,7 @@ Record siProp := SiProp {
siProp_holds :> nat → Prop;
siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
}.
-Arguments siProp_holds : simpl never.
+Global Arguments siProp_holds : simpl never.
Add Printing Constructor siProp.
Declare Scope siProp_scope.
@@ -127,7 +127,7 @@ Definition unseal_eqs :=
Ltac unseal := rewrite !unseal_eqs /=.
Section primitive.
-Arguments siProp_holds !_ _ /.
+Local Arguments siProp_holds !_ _ /.
Notation "P ⊢ Q" := (siProp_entails P Q)
(at level 99, Q at level 200, right associativity).
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 8b03ae742..4705694be 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -192,7 +192,7 @@ values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl ∨ val_is_unboxed v1.
-Arguments vals_compare_safe !_ !_ /.
+Global Arguments vals_compare_safe !_ !_ /.
(** The state: heaps of [option val]s, with [None] representing deallocated locations. *)
Record state : Type := {
@@ -562,11 +562,11 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Definition state_upd_heap (f: gmap loc (option val) → gmap loc (option val)) (σ: state) : state :=
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
-Arguments state_upd_heap _ !_ /.
+Global Arguments state_upd_heap _ !_ /.
Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: state) : state :=
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
-Arguments state_upd_used_proph_id _ !_ /.
+Global Arguments state_upd_used_proph_id _ !_ /.
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc (option val) :=
match vs with
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 85255d127..c095508e8 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -45,7 +45,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
<<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
RET (v, #if decide (v = w1) then true else false) >>>;
}.
-Arguments atomic_heap _ {_}.
+Global Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *)
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index c50ade5de..1b0414e64 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -30,11 +30,11 @@ Structure lock Σ `{!heapG Σ} := Lock {
{{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
}.
-Arguments newlock {_ _} _.
-Arguments acquire {_ _} _.
-Arguments release {_ _} _.
-Arguments is_lock {_ _} _ _ _ _.
-Arguments locked {_ _} _ _.
+Global Arguments newlock {_ _} _.
+Global Arguments acquire {_ _} _.
+Global Arguments release {_ _} _.
+Global Arguments is_lock {_ _} _ _ _ _.
+Global Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 4733b9f9d..9f2b36e04 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -12,7 +12,7 @@ Definition val := Z.
Record heapProp := HeapProp {
heapProp_holds :> gmap loc val → Prop;
}.
-Arguments heapProp_holds : simpl never.
+Global Arguments heapProp_holds : simpl never.
Add Printing Constructor heapProp.
Section ofe.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 1ed8a4882..d1de99fbb 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -128,9 +128,9 @@ Definition read : val := λ: "l", !"l".
Inductive M := Auth : nat → M | Frag : nat → M | Bot.
Section M.
- Arguments cmra_op _ !_ !_/.
- Arguments op _ _ !_ !_/.
- Arguments core _ _ !_/.
+ Local Arguments cmra_op _ !_ !_/.
+ Local Arguments op _ _ !_ !_/.
+ Local Arguments core _ _ !_/.
Canonical Structure M_O : ofeT := leibnizO M.
--
GitLab