From 20e5effc49fa44213aaaaa9cfc6b6edf87283bbb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 May 2023 15:03:48 +0200
Subject: [PATCH] add locality annotation to all Typeclasses Opaque/Transparent
---
_CoqProject | 2 --
coq-lint.sh | 2 +-
iris/algebra/auth.v | 2 +-
iris/algebra/big_op.v | 2 +-
iris/algebra/lib/dfrac_agree.v | 2 +-
iris/algebra/lib/excl_auth.v | 2 +-
iris/algebra/lib/frac_auth.v | 2 +-
iris/algebra/lib/gmap_view.v | 2 +-
iris/algebra/lib/mono_Z.v | 2 +-
iris/algebra/lib/mono_list.v | 2 +-
iris/algebra/lib/mono_nat.v | 2 +-
iris/algebra/lib/ufrac_auth.v | 2 +-
iris/algebra/max_prefix_list.v | 2 +-
iris/algebra/ofe.v | 6 +++---
iris/algebra/vector.v | 2 +-
iris/algebra/view.v | 2 +-
iris/base_logic/lib/boxes.v | 2 +-
iris/base_logic/lib/cancelable_invariants.v | 2 +-
iris/base_logic/lib/gen_inv_heap.v | 2 +-
iris/base_logic/lib/na_invariants.v | 2 +-
iris/base_logic/lib/saved_prop.v | 2 +-
iris/base_logic/lib/wsat.v | 6 +++---
iris/bi/big_op.v | 2 +-
iris/bi/derived_connectives.v | 16 ++++++++--------
iris/bi/embedding.v | 2 +-
iris/bi/interface.v | 2 +-
iris/bi/internal_eq.v | 2 +-
iris/bi/lib/atomic.v | 2 +-
iris/bi/lib/core.v | 2 +-
iris/bi/lib/laterable.v | 2 +-
iris/bi/lib/relations.v | 6 +++---
iris/bi/plainly.v | 4 ++--
iris/bi/updates.v | 4 ++--
iris/program_logic/ownp.v | 2 +-
iris_deprecated/base_logic/auth.v | 2 +-
iris_deprecated/base_logic/sts.v | 4 ++--
iris_heap_lang/derived_laws.v | 2 +-
iris_heap_lang/lib/logatom_lock.v | 2 +-
iris_heap_lang/lib/spawn.v | 2 +-
iris_heap_lang/lib/spin_lock.v | 2 +-
iris_heap_lang/lib/ticket_lock.v | 2 +-
41 files changed, 56 insertions(+), 58 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 8e5eb8ac8..eb848e99c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,8 +15,6 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
# Disabling warnings about future coercion syntax that requires Coq 8.17
# (https://github.com/coq/coq/pull/16230)
-arg -w -arg -future-coercion-class-field
diff --git a/coq-lint.sh b/coq-lint.sh
index e11f0a875..25fdf595a 100755
--- a/coq-lint.sh
+++ b/coq-lint.sh
@@ -4,7 +4,7 @@ set -e
FILE="$1"
-if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
echo "Please add 'Global' or 'Local' as appropriate."
echo
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 369315fca..68ff44ba9 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -65,7 +65,7 @@ Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
Definition auth_auth {A: ucmra} : dfrac → A → auth A := view_auth.
Definition auth_frag {A: ucmra} : A → auth A := view_frag.
-Typeclasses Opaque auth_auth auth_frag.
+Global Typeclasses Opaque auth_auth auth_frag.
Global Instance: Params (@auth_auth) 2 := {}.
Global Instance: Params (@auth_frag) 1 := {}.
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index e68e2ed14..3138cf336 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -27,7 +27,7 @@ Fixpoint big_opL {M : ofe} {o : M → M → M} `{!Monoid o} {A} (f : nat → A
end.
Global Instance: Params (@big_opL) 4 := {}.
Global Arguments big_opL {M} o {_ A} _ !_ /.
-Typeclasses Opaque big_opL.
+Global 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,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index ed13d9e04..88d4178dc 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -132,5 +132,5 @@ Global Instance dfrac_agreeRF_contractive F :
oFunctorContractive F → rFunctorContractive (dfrac_agreeRF F).
Proof. apply _. Qed.
-Typeclasses Opaque to_dfrac_agree.
+Global Typeclasses Opaque to_dfrac_agree.
(* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index f947a7cb8..d245aaeae 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -16,7 +16,7 @@ Definition excl_auth_auth {A : ofe} (a : A) : excl_authR A :=
Definition excl_auth_frag {A : ofe} (a : A) : excl_authR A :=
â—¯ (Some (Excl a)).
-Typeclasses Opaque excl_auth_auth excl_auth_frag.
+Global Typeclasses Opaque excl_auth_auth excl_auth_frag.
Global Instance: Params (@excl_auth_auth) 1 := {}.
Global Instance: Params (@excl_auth_frag) 2 := {}.
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 38e07b42e..094d558b0 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -19,7 +19,7 @@ Definition frac_auth_auth {A : cmra} (x : A) : frac_authR A :=
Definition frac_auth_frag {A : cmra} (q : frac) (x : A) : frac_authR A :=
â—¯ (Some (q,x)).
-Typeclasses Opaque frac_auth_auth frac_auth_frag.
+Global Typeclasses Opaque frac_auth_auth frac_auth_frag.
Global Instance: Params (@frac_auth_auth) 1 := {}.
Global Instance: Params (@frac_auth_frag) 2 := {}.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index abff73761..b009bdcbf 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -526,4 +526,4 @@ Global Instance gmap_viewRF_contractive (K : Type) `{Countable K} F :
oFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.
-Typeclasses Opaque gmap_view_auth gmap_view_frag.
+Global Typeclasses Opaque gmap_view_auth gmap_view_frag.
diff --git a/iris/algebra/lib/mono_Z.v b/iris/algebra/lib/mono_Z.v
index ab4ab1d2a..8c3a824c1 100644
--- a/iris/algebra/lib/mono_Z.v
+++ b/iris/algebra/lib/mono_Z.v
@@ -120,4 +120,4 @@ Section mono_Z.
Qed.
End mono_Z.
-Typeclasses Opaque mono_Z_auth mono_Z_lb.
+Global Typeclasses Opaque mono_Z_auth mono_Z_lb.
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index 16604065a..887239cc1 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -14,7 +14,7 @@ Definition mono_list_lb {A : ofe} (l : list A) : mono_listR A :=
â—¯ (to_max_prefix_list l).
Global Instance: Params (@mono_list_auth) 2 := {}.
Global Instance: Params (@mono_list_lb) 1 := {}.
-Typeclasses Opaque mono_list_auth mono_list_lb.
+Global Typeclasses Opaque mono_list_auth mono_list_lb.
Notation "â—ML dq l" := (mono_list_auth dq l)
(at level 20, dq custom dfrac at level 1, format "â—ML dq l").
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index eb3c52146..3445ce154 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -116,4 +116,4 @@ Section mono_nat.
Qed.
End mono_nat.
-Typeclasses Opaque mono_nat_auth mono_nat_lb.
+Global Typeclasses Opaque mono_nat_auth mono_nat_lb.
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index 9e7abad05..1c79b6445 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -37,7 +37,7 @@ Definition ufrac_auth_auth {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
Definition ufrac_auth_frag {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
â—¯ (Some (q : ufracR,x)).
-Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
+Global Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
Global Instance: Params (@ufrac_auth_auth) 2 := {}.
Global Instance: Params (@ufrac_auth_frag) 2 := {}.
diff --git a/iris/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
index 373463caa..0b77a925b 100644
--- a/iris/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -12,7 +12,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.
Global Instance: Params (@to_max_prefix_list) 1 := {}.
-Typeclasses Opaque to_max_prefix_list.
+Global Typeclasses Opaque to_max_prefix_list.
Section max_prefix_list.
Context {A : ofe}.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 9949147a4..64e454a5c 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -893,7 +893,7 @@ Global Instance uncurry4_ne {A B C D E : ofe} n :
Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
(≡{n}@{A*B*C*D}≡) ==> (≡{n}@{E}≡)) uncurry4 := _.
-Typeclasses Opaque prod_dist.
+Global Typeclasses Opaque prod_dist.
Global Instance prod_map_ne {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
@@ -1087,7 +1087,7 @@ Section sum.
End sum.
Global Arguments sumO : clear implicits.
-Typeclasses Opaque sum_dist.
+Global Typeclasses Opaque sum_dist.
Global Instance sum_map_ne {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
@@ -1278,7 +1278,7 @@ Section option.
Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed.
End option.
-Typeclasses Opaque option_dist.
+Global Typeclasses Opaque option_dist.
Global Arguments optionO : clear implicits.
Global Instance option_fmap_ne {A B : ofe} n:
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index 4ac70ea3c..4f2094cbc 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -36,7 +36,7 @@ Section ofe.
End ofe.
Global Arguments vecO : clear implicits.
-Typeclasses Opaque vec_dist.
+Global Typeclasses Opaque vec_dist.
Section proper.
Context {A : ofe}.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index cdc2b6425..303430eb3 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -87,7 +87,7 @@ Global Instance: Params (@view_frag_proj) 3 := {}.
Definition view_auth {A B} {rel : view_rel A B} (dq : dfrac) (a : A) : view rel :=
View (Some (dq, to_agree a)) ε.
Definition view_frag {A B} {rel : view_rel A B} (b : B) : view rel := View None b.
-Typeclasses Opaque view_auth view_frag.
+Global Typeclasses Opaque view_auth view_frag.
Global Instance: Params (@view_auth) 3 := {}.
Global Instance: Params (@view_frag) 3 := {}.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 6ea0fe6a5..3cbbbfb09 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -308,4 +308,4 @@ Proof.
Qed.
End box.
-Typeclasses Opaque slice box.
+Global Typeclasses Opaque slice box.
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index bd26b84d0..913ddb925 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -160,4 +160,4 @@ Section proofs.
Qed.
End proofs.
-Typeclasses Opaque cinv_own cinv.
+Global Typeclasses Opaque cinv_own cinv.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 51412d1e2..06946752d 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -285,4 +285,4 @@ Section inv_heap.
End inv_heap.
-Typeclasses Opaque inv_heap_inv inv_mapsto inv_mapsto_own.
+Global Typeclasses Opaque inv_heap_inv inv_mapsto inv_mapsto_own.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 0c549c2a0..dc72c7ca8 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -29,7 +29,7 @@ Section defs.
End defs.
Global Instance: Params (@na_inv) 3 := {}.
-Typeclasses Opaque na_own na_inv.
+Global Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{!invGS_gen hlc Σ, !na_invG Σ}.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 01030b170..1571af345 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -25,7 +25,7 @@ Proof. solve_inG. Qed.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (dq : dfrac) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_dfrac_agree dq x).
-Typeclasses Opaque saved_anything_own.
+Global Typeclasses Opaque saved_anything_own.
Global Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index c39b636b6..82016da2c 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -36,18 +36,18 @@ Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
Next P.
Definition ownI `{!wsatGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
-Typeclasses Opaque ownI.
+Global Typeclasses Opaque ownI.
Global Instance: Params (@invariant_unfold) 1 := {}.
Global Instance: Params (@ownI) 3 := {}.
Definition ownE `{!wsatGS Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
-Typeclasses Opaque ownE.
+Global Typeclasses Opaque ownE.
Global Instance: Params (@ownE) 3 := {}.
Definition ownD `{!wsatGS Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
-Typeclasses Opaque ownD.
+Global Typeclasses Opaque ownD.
Global Instance: Params (@ownD) 3 := {}.
Definition wsat `{!wsatGS Σ} : iProp Σ :=
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 5165c6757..31957e495 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -48,7 +48,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
end%I.
Global Instance: Params (@big_sepL2) 3 := {}.
Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
-Typeclasses Opaque big_sepL2.
+Global Typeclasses Opaque big_sepL2.
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
(big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope.
Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index a5071e78a..a5f5d62b3 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -22,7 +22,7 @@ Global Instance: Params (@Persistent) 1 := {}.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
Global Arguments bi_affinely {_} _%I : simpl never.
Global Instance: Params (@bi_affinely) 1 := {}.
-Typeclasses Opaque bi_affinely.
+Global Typeclasses Opaque bi_affinely.
Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
@@ -33,7 +33,7 @@ Global Hint Mode Affine + ! : typeclass_instances.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
Global Arguments bi_absorbingly {_} _%I : simpl never.
Global Instance: Params (@bi_absorbingly) 1 := {}.
-Typeclasses Opaque bi_absorbingly.
+Global Typeclasses Opaque bi_absorbingly.
Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
@@ -45,35 +45,35 @@ Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <pers> P else P)%I.
Global Arguments bi_persistently_if {_} !_ _%I /.
Global Instance: Params (@bi_persistently_if) 2 := {}.
-Typeclasses Opaque bi_persistently_if.
+Global 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.
Global Arguments bi_affinely_if {_} !_ _%I /.
Global Instance: Params (@bi_affinely_if) 2 := {}.
-Typeclasses Opaque bi_affinely_if.
+Global 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.
Global Arguments bi_absorbingly_if {_} !_ _%I /.
Global Instance: Params (@bi_absorbingly_if) 2 := {}.
-Typeclasses Opaque bi_absorbingly_if.
+Global 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.
Global Arguments bi_intuitionistically {_} _%I : simpl never.
Global Instance: Params (@bi_intuitionistically) 1 := {}.
-Typeclasses Opaque bi_intuitionistically.
+Global 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.
Global Arguments bi_intuitionistically_if {_} !_ _%I /.
Global Instance: Params (@bi_intuitionistically_if) 2 := {}.
-Typeclasses Opaque bi_intuitionistically_if.
+Global Typeclasses Opaque bi_intuitionistically_if.
Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
@@ -90,7 +90,7 @@ Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := ▷ False ∨ P.
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.
+Global Typeclasses Opaque bi_except_0.
Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
Global Arguments Timeless {_} _%I : simpl never.
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 21fe9145e..c2c3ad9ab 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -15,7 +15,7 @@ Class Embed (A B : Type) := embed : A → B.
Global Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
Global Instance: Params (@embed) 3 := {}.
-Typeclasses Opaque embed.
+Global Typeclasses Opaque embed.
Global Hint Mode Embed ! - : typeclass_instances.
Global Hint Mode Embed - ! : typeclass_instances.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index a905be189..f2108ee94 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -284,7 +284,7 @@ Notation "â–· P" := (bi_later P) : bi_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
Global Arguments bi_emp_valid {_} _%I : simpl never.
-Typeclasses Opaque bi_emp_valid.
+Global Typeclasses Opaque bi_emp_valid.
Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
Notation "'⊢@{' PROP } Q" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 1e7b3526a..796aa71d5 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -16,7 +16,7 @@ Class InternalEq (PROP : Type) :=
Global Arguments internal_eq {_ _ _} _ _ : simpl never.
Global Hint Mode InternalEq ! : typeclass_instances.
Global Instance: Params (@internal_eq) 3 := {}.
-Typeclasses Opaque internal_eq.
+Global Typeclasses Opaque internal_eq.
Infix "≡" := internal_eq : bi_scope.
Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 45be2a8f7..b37df02b9 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -452,4 +452,4 @@ Tactic Notation "iAaccIntro" "with" constr(sel) :=
end.
(* From here on, prevent TC search from implicitly unfolding these. *)
-Typeclasses Opaque atomic_acc atomic_update.
+Global Typeclasses Opaque atomic_acc atomic_update.
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index def486ff0..8ff8e5fda 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -11,7 +11,7 @@ Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
using conjunction/implication here. *)
∀ Q : PROP, <affine> ■(Q -∗ <pers> Q) -∗ <affine> ■(P -∗ Q) -∗ Q.
Global Instance: Params (@coreP) 1 := {}.
-Typeclasses Opaque coreP.
+Global Typeclasses Opaque coreP.
Section core.
Context {PROP : bi} `{!BiPlainly PROP}.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 14ad4a15f..94fd101c5 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -252,4 +252,4 @@ Section instances.
End instances.
-Typeclasses Opaque make_laterable.
+Global Typeclasses Opaque make_laterable.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 82de7ff37..ad42b9b9f 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -21,7 +21,7 @@ Section definitions.
bi_least_fixpoint (bi_rtc_pre R x2) x1.
Global Instance: Params (@bi_rtc) 4 := {}.
- Typeclasses Opaque bi_rtc.
+ Global Typeclasses Opaque bi_rtc.
Local Definition bi_tc_pre (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
@@ -32,7 +32,7 @@ Section definitions.
bi_least_fixpoint (bi_tc_pre R x2) x1.
Global Instance: Params (@bi_tc) 4 := {}.
- Typeclasses Opaque bi_tc.
+ Global Typeclasses Opaque bi_tc.
(** Reductions of exactly [n] steps. *)
Fixpoint bi_nsteps (R : A → A → PROP) (n : nat) (x1 x2 : A) : PROP :=
@@ -42,7 +42,7 @@ Section definitions.
end.
Global Instance: Params (@bi_nsteps) 5 := {}.
- Typeclasses Opaque bi_nsteps.
+ Global Typeclasses Opaque bi_nsteps.
End definitions.
Local Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index a8a50b3d6..07aef3987 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -15,7 +15,7 @@ Class Plainly (PROP : Type) := plainly : PROP → PROP.
Global Arguments plainly {PROP}%type_scope {_} _%I.
Global Hint Mode Plainly ! : typeclass_instances.
Global Instance: Params (@plainly) 2 := {}.
-Typeclasses Opaque plainly.
+Global Typeclasses Opaque plainly.
Notation "â– P" := (plainly P) : bi_scope.
@@ -112,7 +112,7 @@ Definition plainly_if {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP
(if p then â– P else P)%I.
Global Arguments plainly_if {_ _} !_ _%I /.
Global Instance: Params (@plainly_if) 2 := {}.
-Typeclasses Opaque plainly_if.
+Global Typeclasses Opaque plainly_if.
Notation "â– ? p P" := (plainly_if p P) : bi_scope.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 8c6a60621..deb35e594 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -17,7 +17,7 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
Global Instance : Params (@bupd) 2 := {}.
Global Hint Mode BUpd ! : typeclass_instances.
Global Arguments bupd {_}%type_scope {_} _%bi_scope.
-Typeclasses Opaque bupd.
+Global Typeclasses Opaque bupd.
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
@@ -27,7 +27,7 @@ Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
Global Instance: Params (@fupd) 4 := {}.
Global Hint Mode FUpd ! : typeclass_instances.
Global Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
-Typeclasses Opaque fupd.
+Global Typeclasses Opaque fupd.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index bcfbfc14c..842e8520a 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -46,7 +46,7 @@ Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP `{!ownPGS Λ Σ} (σ : state Λ) : iProp Σ :=
own ownP_name (◯E σ).
-Typeclasses Opaque ownP.
+Global Typeclasses Opaque ownP.
Global Instance: Params (@ownP) 3 := {}.
(* Adequacy *)
diff --git a/iris_deprecated/base_logic/auth.v b/iris_deprecated/base_logic/auth.v
index da152d3bf..303e36405 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -60,7 +60,7 @@ Section definitions.
Proof. apply _. Qed.
End definitions.
-Typeclasses Opaque auth_own auth_inv auth_ctx.
+Global Typeclasses Opaque auth_own auth_inv auth_ctx.
Global Instance: Params (@auth_own) 4 := {}.
Global Instance: Params (@auth_inv) 5 := {}.
Global Instance: Params (@auth_ctx) 7 := {}.
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index 631d00e0d..642fc5ab7 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -118,7 +118,7 @@ Section sts.
- apply sts.closed_up; set_solver.
Qed.
- Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
+ Local Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
Lemma sts_alloc φ E N s :
▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
@@ -181,4 +181,4 @@ Section sts.
Proof. by apply sts_accS. Qed.
End sts.
-Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
+Global Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 71858a63a..f9a7ee714 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -407,4 +407,4 @@ Qed.
End lifting.
-Typeclasses Opaque array.
+Global Typeclasses Opaque array.
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index cb6d7c23c..6daea74fa 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -101,4 +101,4 @@ Section tada.
End tada.
-Typeclasses Opaque tada_is_lock tada_lock_state.
+Global Typeclasses Opaque tada_is_lock tada_lock_state.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index dfb8d2778..0d5fea58c 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -76,4 +76,4 @@ Proof.
Qed.
End proof.
-Typeclasses Opaque join_handle.
+Global Typeclasses Opaque join_handle.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 338c25acf..5218861f6 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -102,7 +102,7 @@ Section proof.
Qed.
End proof.
-Typeclasses Opaque is_lock locked.
+Global Typeclasses Opaque is_lock locked.
Canonical Structure spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
{| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 7a42b151b..0827bcd7d 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -172,7 +172,7 @@ Section proof.
Qed.
End proof.
-Typeclasses Opaque is_lock issued locked.
+Global Typeclasses Opaque is_lock issued locked.
Canonical Structure ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
{| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
--
GitLab