From 9c0037c698973aa55f1b5252a12fae040cc06839 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 2 Mar 2022 00:49:44 +0100
Subject: [PATCH] Make `inG` instances local

---
 iris/base_logic/lib/boxes.v                 | 3 ++-
 iris/base_logic/lib/cancelable_invariants.v | 3 ++-
 iris/base_logic/lib/gen_heap.v              | 3 ++-
 iris/base_logic/lib/gen_inv_heap.v          | 3 ++-
 iris/base_logic/lib/ghost_map.v             | 3 ++-
 iris/base_logic/lib/ghost_var.v             | 3 ++-
 iris/base_logic/lib/gset_bij.v              | 3 ++-
 iris/base_logic/lib/mono_nat.v              | 3 ++-
 iris/base_logic/lib/na_invariants.v         | 3 ++-
 iris/base_logic/lib/saved_prop.v            | 3 ++-
 iris/base_logic/lib/wsat.v                  | 6 +++---
 iris/program_logic/ownp.v                   | 6 ++++--
 iris_deprecated/base_logic/auth.v           | 3 ++-
 iris_deprecated/base_logic/sts.v            | 3 ++-
 iris_heap_lang/lib/counter.v                | 6 ++++--
 iris_heap_lang/lib/spawn.v                  | 3 ++-
 iris_heap_lang/lib/spin_lock.v              | 3 ++-
 iris_heap_lang/lib/ticket_lock.v            | 3 ++-
 iris_staging/base_logic/mono_list.v         | 3 ++-
 tests/ipm_paper.v                           | 3 ++-
 tests/one_shot.v                            | 3 ++-
 tests/one_shot_once.v                       | 3 ++-
 22 files changed, 49 insertions(+), 26 deletions(-)

diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index f86854d37..252446481 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -6,9 +6,10 @@ Import uPred.
 
 (** The CMRAs we need. *)
 Class boxG Σ :=
-  boxG_inG :> inG Σ (prodR
+  boxG_inG : inG Σ (prodR
     (excl_authR boolO)
     (optionR (agreeR (laterO (iPropO Σ))))).
+Local Existing Instance boxG_inG.
 
 Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
                                             optionRF (agreeRF (▶ ∙)) ) ].
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 0f6c3804c..2515ed6be 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -5,8 +5,9 @@ From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG Σ := cinv_inG :> inG Σ fracR.
+Class cinvG Σ := cinv_inG : inG Σ fracR.
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
+Local Existing Instance cinv_inG.
 
 Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 7df5ef405..9a41a34bb 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -68,8 +68,9 @@ these can be matched up with the invariant namespaces. *)
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
   gen_heapGpreS_heap :> ghost_mapG Σ L V;
   gen_heapGpreS_meta :> ghost_mapG Σ L gname;
-  gen_heapGpreS_meta_data :> inG Σ (reservation_mapR (agreeR positiveO));
+  gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
 }.
+Local Existing Instance gen_heapGpreS_meta_data.
 
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
   gen_heap_inG :> gen_heapGpreS L V Σ;
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index e3b57bbcf..6545e8730 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -31,8 +31,9 @@ Definition to_inv_heap {L V : Type} `{Countable L}
   prod_map (λ x, Excl' x) to_agree <$> h.
 
 Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  inv_heapGpreS_inG :> inG Σ (authR (inv_heap_mapUR L V))
+  inv_heapGpreS_inG : inG Σ (authR (inv_heap_mapUR L V))
 }.
+Local Existing Instance inv_heapGpreS_inG.
 
 Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
   inv_heap_inG :> inv_heapGpreS L V Σ;
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index ac9a1dc0f..ea559d567 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -12,8 +12,9 @@ From iris.prelude Require Import options.
 FIXME: This is intentionally discrete-only, but
 should we support setoids via [Equiv]? *)
 Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
-  ghost_map_inG :> inG Σ (gmap_viewR K (leibnizO V));
+  ghost_map_inG : inG Σ (gmap_viewR K (leibnizO V));
 }.
+Local Existing Instance ghost_map_inG.
 Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
   #[ GFunctor (gmap_viewR K (leibnizO V)) ].
 
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 625634567..2535b60c2 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -8,8 +8,9 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class ghost_varG Σ (A : Type) := GhostVarG {
-  ghost_var_inG :> inG Σ (dfrac_agreeR $ leibnizO A);
+  ghost_var_inG : inG Σ (dfrac_agreeR $ leibnizO A);
 }.
+Local Existing Instance ghost_var_inG.
 Global Hint Mode ghost_varG - ! : typeclass_instances.
 
 Definition ghost_varΣ (A : Type) : gFunctors :=
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 01eff6928..9be5df415 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -28,8 +28,9 @@ From iris.prelude Require Import options.
 
 (* The uCMRA we need. *)
 Class gset_bijG Σ A B `{Countable A, Countable B} :=
-  GsetBijG { gset_bijG_inG :> inG Σ (gset_bijR A B); }.
+  GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
 Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
+Local Existing Instance gset_bijG_inG.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
   #[ GFunctor (gset_bijR A B) ].
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 99389ea1d..9069f8e3b 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -14,7 +14,8 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 Class mono_natG Σ :=
-  MonoNatG { mono_natG_inG :> inG Σ mono_natR; }.
+  MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
+Local Existing Instance mono_natG_inG.
 Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
 Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 1f32d1134..f4fdd2308 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -9,7 +9,8 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+  na_inv_inG : inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Local Existing Instance na_inv_inG.
 Definition na_invΣ : gFunctors :=
   #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
 Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 85df42832..29a905c12 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -9,9 +9,10 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
+  saved_anything_inG : inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
+Local Existing Instance saved_anything_inG.
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
   #[ GFunctor (agreeRF F) ].
 
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 8667560e6..93e6d4fcf 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -9,9 +9,9 @@ exception of what's in the [invGS] module. The module [invGS] is thus exported i
 [fancy_updates], where [wsat] is only imported. *)
 Module invGS.
   Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
-    invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    invGpreS_enabled :> inG Σ coPset_disjR;
-    invGpreS_disabled :> inG Σ (gset_disjR positive);
+    invGpreS_inv : inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    invGpreS_enabled : inG Σ coPset_disjR;
+    invGpreS_disabled : inG Σ (gset_disjR positive);
   }.
 
   Class invGS (Σ : gFunctors) : Set := InvG {
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 859d05348..34eb93c79 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -16,9 +16,10 @@ union.
 
 Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
   ownP_invG : invGS Σ;
-  ownP_inG :> inG Σ (excl_authR (stateO Λ));
+  ownP_inG : inG Σ (excl_authR (stateO Λ));
   ownP_name : gname;
 }.
+Local Existing Instance ownP_inG.
 
 Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
   iris_invGS := ownP_invG;
@@ -35,8 +36,9 @@ Definition ownPΣ (Λ : language) : gFunctors :=
 
 Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
   ownPPre_invG :> invGpreS Σ;
-  ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
+  ownPPre_state_inG : inG Σ (excl_authR (stateO Λ))
 }.
+Local Existing Instance ownPPre_state_inG.
 
 Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPGpreS Λ Σ.
 Proof. solve_inG. Qed.
diff --git a/iris_deprecated/base_logic/auth.v b/iris_deprecated/base_logic/auth.v
index 451cf54e1..c1144c0e1 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -11,9 +11,10 @@ Import uPred.
 
 (* The CMRA we need. *)
 Class authG Σ (A : ucmra) := AuthG {
-  auth_inG :> inG Σ (authR A);
+  auth_inG : inG Σ (authR A);
   auth_cmra_discrete :> CmraDiscrete A;
 }.
+Local Existing Instance auth_inG.
 Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
 
 Global Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index b8047cea7..631d00e0d 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -10,9 +10,10 @@ Import uPred.
 
 (** The CMRA we need. *)
 Class stsG Σ (sts : stsT) := StsG {
-  sts_inG :> inG Σ (sts_resR sts);
+  sts_inG : inG Σ (sts_resR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
+Local Existing Instance sts_inG.
 
 Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (sts_resR sts) ].
 Global Instance subG_stsΣ Σ sts :
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 8d19bd9e3..d89e8bd22 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -13,7 +13,8 @@ Definition incr : val := rec: "incr" "l" :=
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
-Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR max_natUR) }.
+Class mcounterG Σ := MCounterG { mcounter_inG : inG Σ (authR max_natUR) }.
+Local Existing Instance mcounter_inG.
 Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
 Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
@@ -86,7 +87,8 @@ End mono_proof.
 
 (** Counter with contributions *)
 Class ccounterG Σ :=
-  CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
+  CCounterG { ccounter_inG : inG Σ (frac_authR natR) }.
+Local Existing Instance ccounter_inG.
 Definition ccounterΣ : gFunctors :=
   #[GFunctor (frac_authR natR)].
 
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 75b7aac74..e7fd2a47f 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -19,7 +19,8 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (exclR unitO) }.
+Local Existing Instance spawn_tokG.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index fe600a2a5..f1fe32924 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -14,7 +14,8 @@ Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
+Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
+Local Existing Instance lock_tokG.
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 31ddba659..ea3321c70 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -28,7 +28,8 @@ Definition release : val :=
 
 (** The CMRAs we need. *)
 Class tlockG Σ :=
-  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
+  tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
+Local Existing Instance tlock_G.
 Definition tlockΣ : gFunctors :=
   #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
 
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index ec4ffa575..5fa218e56 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -22,7 +22,8 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 Class mono_listG (A : Type) Σ :=
-  MonoListG { mono_list_inG :> inG Σ (mono_listR (leibnizO A)) }.
+  MonoListG { mono_list_inG : inG Σ (mono_listR (leibnizO A)) }.
+Local Existing Instance mono_list_inG.
 Definition mono_listΣ (A : Type) : gFunctors :=
   #[GFunctor (mono_listR (leibnizO A))].
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 3bc0914b3..4f16c146f 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -188,7 +188,8 @@ Section M.
   Qed.
 End M.
 
-Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
+Class counterG Σ := CounterG { counter_tokG : inG Σ M_UR }.
+Local Existing Instance counter_tokG.
 Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
 Global Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index c5ca6dbb9..f46d470a5 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -31,7 +31,8 @@ Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
 Definition Pending : one_shotR := Cinl (Excl ()).
 Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instance one_shot_inG.
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. solve_inG. Qed.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 7df7a2384..f2bceed69 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -28,7 +28,8 @@ Definition one_shotR := csumR fracR (agreeR ZO).
 Definition Pending (q : Qp) : one_shotR := Cinl q.
 Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instance one_shot_inG.
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. solve_inG. Qed.
-- 
GitLab