diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 5e4e603488b713b3e55b9088b6e3144a914eecf8..1da235b8b184ed35cff232603e18960a2c356900 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -99,9 +99,10 @@ for further details on `libG` classes).  For example, the STS library is
 parameterized by an STS and assumes that the STS state space is inhabited:
 ```coq
 Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
+  sts_inG : inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
+Local Existing Instance sts_inG.
 ```
 In this case, the `Instance` for this `libG` class has more than just a `subG`
 assumption:
diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 3fc047bf5f2991fcf657b351ad865d3fe4ff3163..71d547b323487e7b8632aa9dd19c098cb43f64e4 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -14,12 +14,20 @@ Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
 not have to expose to clients what exactly their resource algebras are. For
 example, in the [one-shot example](../tests/one_shot.v), we have:
 ```coq
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instances one_shot_inG.
 ```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
+Here, the projection `one_shot_inG` is registered as an instance for type-class
+resolution. If you need several resource algebras, just add more `inG` fields.
+If you are using another module as part of yours, add a field like
+`one_shot_other : otherG Σ`. All of these fields should be added to the
+`Local Existing Instances` command.
+
+The code above enables these typeclass instances only in the surrounding file
+where they are used to define the new abstractions by the library. The
+interface of these abstractions will only depend on the `one_shotG` class.
+Since `one_shot_inG` will be hidden from clients, they will not accidentally
+rely on it in their code.
 
 Having defined the type class, we need to provide a way to instantiate it.  This
 is an important step, as not every resource algebra can actually be used: if
@@ -118,12 +126,14 @@ class for the generalized heap module, bundles the usual `inG` assumptions
 together with the `gname`:
 ```coq
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heapGpreS_heap :> ghost_mapG Σ L V;
+  gen_heapGpreS_heap : ghost_mapG Σ L V;
 }.
+Local Existing Instances gen_heapGpreS_heap.
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG :> gen_heapGpreS L V Σ;
+  gen_heap_inG : gen_heapGpreS L V Σ;
   gen_heap_name : gname;
 }.
+Local Existing Instances gen_heap_inG.
 ```
 The trailing `S` here is for "singleton", because the idea is that only one
 instance of `gen_heapGS` ever exists. This is important, since two instances
@@ -273,7 +283,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
 your example would look as follows:
 
 ```coq
-Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Local Existing Instance lib_inG.
+
 Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index f86854d379282b82a437ca51e60a253a7424b606..25244648195ea43591ef1b99de4b77c0b8772d66 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 0f6c3804c99255fc1417477f55248797ba92907b..5eba9f038fa85248333233cf78eef5d888ed7a14 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -5,7 +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 }.
+Local Existing Instance cinv_inG.
+
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
 
 Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 7df5ef405a90123ef77dca3a226b8f9d53417092..7aa2d54cb74ad1f40584d6117ad028c87672b353 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -66,16 +66,18 @@ these can be matched up with the invariant namespaces. *)
 (** The CMRAs we need, and the global ghost names we are using. *)
 
 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_heap : ghost_mapG Σ L V;
+  gen_heapGpreS_meta : ghost_mapG Σ L gname;
+  gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
 }.
+Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
 
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG :> gen_heapGpreS L V Σ;
+  gen_heap_inG : gen_heapGpreS L V Σ;
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
+Local Existing Instance gen_heap_inG.
 Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
 Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
 Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index e3b57bbcf5238a3022ea7a24523175d8ce36abee..127ae29235bb2b19e55a2c8b233b0b57e026a6db 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -31,13 +31,15 @@ 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 Σ;
+  inv_heap_inG : inv_heapGpreS L V Σ;
   inv_heap_name : gname
 }.
+Local Existing Instance inv_heap_inG.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
 Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index ac9a1dc0f5901242d0e43054ab530630463a9834..a64159b000da7d33b1d2ae179c3c8c0045623f6d 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -12,8 +12,10 @@ 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 6256345671815a77ef9e761079dc1beb4988b6ce..2535b60c24d357e22d2eb5915fbf2affe13e22d3 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 01eff6928c3000667b98bf8930661b868bbd006a..402144c42b7b012b0eaee2d34521d49ea6dec368 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -28,7 +28,8 @@ 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); }.
+Local Existing Instance gset_bijG_inG.
 Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 99389ea1d11c82650061c9a2e39cca5eae6eb45b..95d6555e1dfe71d49c217097fa12b9e538f2ea31 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -14,7 +14,9 @@ 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 1f32d113451280ee092e0866661fd695921ecb88..c6b701d92c90321c8ad983e0b4baf2df4cecd001 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -9,7 +9,9 @@ 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/proph_map.v b/iris/base_logic/lib/proph_map.v
index 98693dd34c62fe96599fb5f02f3aa857ada4cdd7..f405fa14fa3ebc9b1299dee9cf685472d3a6604b 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -9,14 +9,16 @@ Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
 Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
-  proph_map_GpreS_inG :> ghost_mapG Σ P (list V)
+  proph_map_GpreS_inG : ghost_mapG Σ P (list V)
 }.
+Local Existing Instances proph_map_GpreS_inG.
 
 Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
-  proph_map_inG :> proph_mapGpreS P V Σ;
+  proph_map_inG : proph_mapGpreS P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
+Local Existing Instances proph_map_inG.
 
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[ghost_mapΣ P (list V)].
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 85df428322e515b911e47da80d24912e3615484a..2e3a1733904477c0a16c6ca6878a97d6cab28a85 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -9,9 +9,11 @@ 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 8667560e652691d2e76afe4f3dbd80e738930bc3..e6e9e1e81a35c33976725a24844bf35cb13228ab 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -9,13 +9,13 @@ 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 {
-    inv_inG :> invGpreS Σ;
+    inv_inG : invGpreS Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
@@ -30,6 +30,7 @@ Module invGS.
   Proof. solve_inG. Qed.
 End invGS.
 Import invGS.
+Local Existing Instances inv_inG invGpreS_inv invGpreS_enabled invGpreS_disabled.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 859d053482cf8a9059a65fb1cf3e4bf21edeee84..34eb93c7969a638489d56be44f474a99bf020f28 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 451cf54e1a46fb0d743a0052a98b1049ecd6cdd2..da152d3bfb78a02be7c4edf5444d9f2df3698306 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -11,9 +11,11 @@ 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 b8047cea765faffe88dbf6f4214cfd3edfd3799a..631d00e0d1b3e5859934a8c1d18b994741ade932 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 8d19bd9e345c03b2663c60c8f200d1bd65057508..cb6312aaccae86bea641bce0511a3d63ec5bb2f3 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -13,7 +13,9 @@ 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 +88,9 @@ 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 75b7aac74284bea68c5b613c03b1ec055c688877..70573628927101a2b11bd4b6f6c1a7f5c0a0e93f 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -19,7 +19,9 @@ 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 fe600a2a51d1b5b8e552db6503e13154fd383692..6b0ab568bf41dcbe1ce54f43b366fac7abbef558 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -14,7 +14,9 @@ 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 31ddba65967f107329fd884d98736686e9908ff6..c52b35e3d6abfa88c18117c7370a33ae74a80d5e 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -28,7 +28,9 @@ 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 ec4ffa575b8522fe579b3cdd64ba4e406acec336..6bb43fa67f38b78674d64ec36306d48f44bd10fd 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -22,7 +22,9 @@ 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 3bc0914b39d9b9fd2cd5d40449874c5429fcaa04..67f4f18e587d1c1783894c625575495a0e717c84 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -188,7 +188,9 @@ 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 c5ca6dbb9359c34f1775c1a1866f039a7a5e948b..378177ec1cac857a5ec8462674ea08494500dc5e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -31,7 +31,9 @@ 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 7df7a238444dc0711c48649a572768e239a39464..506ac4cc71f5ec82f54c09325872fd89242f8e7b 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -28,7 +28,9 @@ 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.