From ff9307a03c90873fa16d3524dc175f9dd902e858 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 May 2021 19:38:19 +0200
Subject: [PATCH] mark Instances as Local/Global
---
Makefile.coq.local | 2 +-
iris/algebra/agree.v | 2 +-
iris/algebra/cmra.v | 4 ++--
iris/algebra/cofe_solver.v | 2 +-
iris/algebra/csum.v | 4 ++--
iris/algebra/dra.v | 6 +++---
iris/algebra/excl.v | 4 ++--
iris/algebra/ofe.v | 6 +++---
iris/algebra/proofmode_classes.v | 2 +-
iris/algebra/sts.v | 4 ++--
iris/base_logic/lib/iprop.v | 2 +-
iris/bi/derived_connectives.v | 2 +-
iris/bi/monpred.v | 2 +-
iris/program_logic/total_weakestpre.v | 2 +-
iris/program_logic/weakestpre.v | 2 +-
iris/proofmode/classes.v | 4 ++--
iris/proofmode/coq_tactics.v | 4 ++--
iris_heap_lang/lib/increment.v | 2 +-
iris_heap_lang/lib/lock.v | 2 +-
iris_heap_lang/locations.v | 2 +-
iris_staging/algebra/max_prefix_list.v | 2 +-
iris_staging/algebra/mono_list.v | 4 ++--
22 files changed, 33 insertions(+), 33 deletions(-)
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 6a0bc8656..f87fa5779 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -16,7 +16,7 @@ test: $(TESTFILES:.v=.vo)
$(SHOW)"Performing some style checks..."
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
- if egrep '^\s*(Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
+ if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\b' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
done
# Make sure main Iris does not import other Iris packages.
$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 66bd3e414..2421f8332 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -86,7 +86,7 @@ Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
end.
Local Instance agree_valid_instance : Valid (agree A) := λ x, ∀ n, ✓{n} x.
-Program Instance agree_op_instance : Op (agree A) := λ x y,
+Local Program Instance agree_op_instance : Op (agree A) := λ x y,
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
Local Instance agree_pcore_instance : PCore (agree A) := Some.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 8c9ca92f2..43a8a068c 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -795,7 +795,7 @@ Record rFunctor := RFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
-Existing Instances rFunctor_map_ne rFunctor_mor.
+Global Existing Instances rFunctor_map_ne rFunctor_mor.
Global Instance: Params (@rFunctor_map) 9 := {}.
Declare Scope rFunctor_scope.
@@ -886,7 +886,7 @@ Record urFunctor := URFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (urFunctor_map fg)
}.
-Existing Instances urFunctor_map_ne urFunctor_mor.
+Global Existing Instances urFunctor_map_ne urFunctor_mor.
Global Instance: Params (@urFunctor_map) 9 := {}.
Declare Scope urFunctor_scope.
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 69fea2571..f2b452fe9 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -6,7 +6,7 @@ Record solution (F : oFunctor) := Solution {
solution_cofe : Cofe solution_car;
solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}.
-Existing Instance solution_cofe.
+Global Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 2d55fd1e3..28209dfb8 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -36,12 +36,12 @@ Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
| Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
| CsumBot_equiv : CsumBot ≡ CsumBot.
-Existing Instance csum_equiv.
+Local Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
| Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
| CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
-Existing Instance csum_dist.
+Local Existing Instance csum_dist.
Global Instance Cinl_ne : NonExpansive (@Cinl A B).
Proof. by constructor. Qed.
diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index b2b7ae201..01ed39ecf 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -44,7 +44,7 @@ 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.
+Global Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
(** Lifting properties from the mixin *)
Section dra_mixin.
@@ -146,10 +146,10 @@ Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
Proof. apply validity_prf. Qed.
Local Hint Resolve validity_valid_car_valid : core.
-Program Instance validity_pcore_instance : PCore (validity A) := λ x,
+Local Program Instance validity_pcore_instance : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) (✓ x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
-Program Instance validity_op_instance : Op (validity A) := λ x y,
+Local Program Instance validity_op_instance : Op (validity A) := λ x y,
Validity (validity_car x â‹… validity_car y)
(✓ x ∧ ✓ y ∧ validity_car x ## validity_car y) _.
Solve Obligations with naive_solver eauto using dra_op_valid.
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 0dec359fb..54646d390 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -29,11 +29,11 @@ Implicit Types x y : excl A.
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
| ExclBot_equiv : ExclBot ≡ ExclBot.
-Existing Instance excl_equiv.
+Local Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
-Existing Instance excl_dist.
+Local Existing Instance excl_dist.
Global Instance Excl_ne : NonExpansive (@Excl A).
Proof. by constructor. Qed.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 01cbd49d8..d743539a6 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -535,7 +535,7 @@ Record ofe_mor (A B : ofe) : Type := OfeMor {
}.
Global Arguments OfeMor {_ _} _ {_}.
Add Printing Constructor ofe_mor.
-Existing Instance ofe_mor_ne.
+Global Existing Instance ofe_mor_ne.
Notation "'λne' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t) _) ..) _)
@@ -710,7 +710,7 @@ Record oFunctor := OFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
-Existing Instance oFunctor_map_ne.
+Global Existing Instance oFunctor_map_ne.
Global Instance: Params (@oFunctor_map) 9 := {}.
Declare Scope oFunctor_scope.
@@ -1329,7 +1329,7 @@ Section iso_cofe_subtype.
Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
- Existing Instance Hgne.
+ Local Existing Instance Hgne.
Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
Program Definition iso_cofe_subtype : Cofe B :=
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 41571ba25..489a9e36c 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -27,7 +27,7 @@ Global Hint Mode IsOp' + ! - - : typeclass_instances.
Global Hint Mode IsOp' + - ! ! : typeclass_instances.
Class IsOp'LR {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
-Existing Instance is_op_lr | 0.
+Global Existing Instance is_op_lr | 0.
Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
Global Instance is_op_lr_op {A : cmra} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 06c86aaf2..88b8cba6e 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -196,7 +196,7 @@ Implicit Types T : tokens sts.
Inductive sts_equiv : Equiv (car sts) :=
| auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
| frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
-Existing Instance sts_equiv.
+Local Existing Instance sts_equiv.
Local Instance sts_valid_instance : Valid (car sts) := λ x,
match x with
| auth s T => tok s ## T
@@ -212,7 +212,7 @@ Inductive sts_disjoint : Disjoint (car sts) :=
(∃ s, s ∈ S1 ∩ S2) → T1 ## T2 → frag S1 T1 ## frag S2 T2
| auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → auth s T1 ## frag S T2
| frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → frag S T1 ## auth s T2.
-Existing Instance sts_disjoint.
+Local Existing Instance sts_disjoint.
Local Instance sts_op_instance : Op (car sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index bccdb42bf..1b2c47ce1 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -29,7 +29,7 @@ Structure gFunctor := GFunctor {
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
Global Arguments GFunctor _ {_}.
-Existing Instance gFunctor_map_contractive.
+Global Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 0027f0f0d..7f965854e 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -32,7 +32,7 @@ Global Hint Mode Affine + ! : typeclass_instances.
Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Global Hint Mode BiAffine ! : typeclass_instances.
-Existing Instance absorbing_bi | 0.
+Global Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 30f159eb8..afda962f8 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -9,7 +9,7 @@ Structure biIndex :=
bi_index_inhabited : Inhabited bi_index_type;
bi_index_rel : SqSubsetEq bi_index_type;
bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
-Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
+Global Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
(* We may want to instantiate monPred with the reflexivity relation in
the case where there is no relevent order. In that case, there is
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index f2fd5b3e1..8b98e91ae 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -62,7 +62,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
Definition twp' := twp_aux.(unseal).
Global Arguments twp' {Λ Σ _}.
-Existing Instance twp'.
+Global 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 883d401af..e3656a5dd 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -78,7 +78,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
Definition wp' := wp_aux.(unseal).
Global Arguments wp' {Λ Σ _}.
-Existing Instance wp'.
+Global Existing Instance wp'.
Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index a57e644d8..88bf16a4a 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -512,7 +512,7 @@ Global Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_0 : AsEmpValid φ P.
Global Arguments AsEmpValid0 {_} _%type _%I.
-Existing Instance as_emp_valid_0 | 0.
+Global Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ → ⊢ P.
@@ -570,7 +570,7 @@ Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
(* The typeclass used for the [iInv] tactic.
Input: [Pinv]
- Arguments:
+ Other Arguments:
- [Pinv] is an invariant assertion
- [Pin] is an additional logic assertion needed for opening an invariant
- [φ] is an additional Coq assertion needed for opening an invariant
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 617d76f43..a2c2007f3 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -931,7 +931,7 @@ Inductive IntoModalIntuitionisticEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 P
| MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
Existing Class IntoModalIntuitionisticEnv.
-Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
+Global Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
(* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
@@ -963,7 +963,7 @@ Inductive IntoModalSpatialEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
| MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
IntoModalSpatialEnv M Γ Γ MIEnvId false.
Existing Class IntoModalSpatialEnv.
-Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
+Global Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
Section tac_modal_intro.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 0fdee4cd0..4887a01cc 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -147,7 +147,7 @@ End increment.
Section increment_client.
Context `{!heapG Σ, !spawnG Σ}.
- Existing Instance primitive_atomic_heap.
+ Local Existing Instance primitive_atomic_heap.
Definition incr_client : val :=
λ: "x",
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 1b0414e64..bc7d88da8 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -36,7 +36,7 @@ Global Arguments release {_ _} _.
Global Arguments is_lock {_ _} _ _ _ _.
Global Arguments locked {_ _} _ _.
-Existing Instances is_lock_ne is_lock_persistent locked_timeless.
+Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Global Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index aae2090d1..a11775e14 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -14,7 +14,7 @@ Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
-Program Instance loc_infinite : Infinite loc :=
+Global Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation. done. Qed.
diff --git a/iris_staging/algebra/max_prefix_list.v b/iris_staging/algebra/max_prefix_list.v
index 715bfac4c..ec1b0c2af 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris_staging/algebra/max_prefix_list.v
@@ -11,7 +11,7 @@ Definition max_prefix_listUR (A : ofe) := gmapUR nat (agreeR A).
Definition to_max_prefix_list {A} (l : list A) : gmap nat (agree A) :=
to_agree <$> map_seq 0 l.
-Instance: Params (@to_max_prefix_list) 1 := {}.
+Global Instance: Params (@to_max_prefix_list) 1 := {}.
Typeclasses Opaque to_max_prefix_list.
Section max_prefix_list.
diff --git a/iris_staging/algebra/mono_list.v b/iris_staging/algebra/mono_list.v
index 7954fa9fb..a41715451 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris_staging/algebra/mono_list.v
@@ -17,8 +17,8 @@ Definition mono_list_auth {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
â—{q} (to_max_prefix_list l) â‹… â—¯ (to_max_prefix_list l).
Definition mono_list_lb {A : ofe} (l : list A) : mono_listR A :=
â—¯ (to_max_prefix_list l).
-Instance: Params (@mono_list_auth) 2 := {}.
-Instance: Params (@mono_list_lb) 1 := {}.
+Global Instance: Params (@mono_list_auth) 2 := {}.
+Global Instance: Params (@mono_list_lb) 1 := {}.
Typeclasses Opaque mono_list_auth mono_list_lb.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
--
GitLab