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..2515ed6be324d038f530cb69be7562cdc20f953e 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 7df5ef405a90123ef77dca3a226b8f9d53417092..9a41a34bb0b259e5e0eaa0e171b5c6edf3c9e1f7 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 e3b57bbcf5238a3022ea7a24523175d8ce36abee..6545e873063aed86e2b54ddd9852c1c0b6cef948 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 ac9a1dc0f5901242d0e43054ab530630463a9834..ea559d567199efc5144a38ca2212d1769cfb42e9 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 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..9be5df415bcd35a60ccec1ba8f21924f155168d4 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 99389ea1d11c82650061c9a2e39cca5eae6eb45b..9069f8e3b2b83feb5a735b684e0b7bb4a2c00173 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 1f32d113451280ee092e0866661fd695921ecb88..f4fdd230833035df794fd6cfd3fa0746a7abf3f0 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 85df428322e515b911e47da80d24912e3615484a..29a905c1211b6aec0ba5ddd8c43d6d0f1c276422 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 8667560e652691d2e76afe4f3dbd80e738930bc3..93e6d4fcfabac379fc8ed6f26547939d5b9d2ebf 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 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..c1144c0e19d5cf332f7ea0e838a7a52d1a970c86 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 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..d89e8bd227349d933e2bddc4eca8093ab9d8416b 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 75b7aac74284bea68c5b613c03b1ec055c688877..e7fd2a47fc231a855e76886a645316d38874f3ed 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 fe600a2a51d1b5b8e552db6503e13154fd383692..f1fe32924b4aa2fa97b5d9f06276a8c7910dd75e 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 31ddba65967f107329fd884d98736686e9908ff6..ea3321c70b2f6877ed8ee83efce5f3470306a6d6 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 ec4ffa575b8522fe579b3cdd64ba4e406acec336..5fa218e562a3a3a0fcf0b35ab2c6bd3f46b04426 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 3bc0914b39d9b9fd2cd5d40449874c5429fcaa04..4f16c146fb1383a8c2461989ac29e32f51394406 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 c5ca6dbb9359c34f1775c1a1866f039a7a5e948b..f46d470a589b9488d50e753dc8b9b339988a29a1 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 7df7a238444dc0711c48649a572768e239a39464..f2bceed693d43b8de58667a05f3a9b2999f3fc01 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.