diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index e5781758c5023669ebccb95017310a1476b2adff..ab2b264a094e932eca5a67d778d19f1d3c07f121 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -99,10 +99,9 @@ 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);
+  #[local] 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 bd9d65f88e742354b7e18eeb6c76bf6b6e763bd8..1795344f52f8866c87847f44b55d9b4cebf5b6b1 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -126,14 +126,13 @@ 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;
+  #[local] 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 Σ;
+  #[local] 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
@@ -283,8 +282,8 @@ 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 Σ))))) }.
-Local Existing Instance lib_inG.
+Class libG Σ :=
+  { #[local] lib_inG :: inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
 
 Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index ec1163a1579a72465509d83a892ae2a23ffb8068..87872b494be8414a214343decc6e732306e889b0 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -6,10 +6,9 @@ Import uPred.
 
 (** The CMRAs we need. *)
 Class boxG Σ :=
-  boxG_inG : inG Σ (prodR
+  #[local] 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 e9df6b26d52aad304753036e35b16db6fd55f04a..d11c0534ce621c1c2ca95c19deef3ffe914d8c02 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -5,8 +5,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG Σ := { cinv_inG : inG Σ fracR }.
-Local Existing Instance cinv_inG.
+Class cinvG Σ := { #[local] cinv_inG :: inG Σ fracR }.
 
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
 
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index d521738fea793efa8097e7d27fe4111134de005c..3aa0c1f18c5f6e94cc0519eb6665217f6e3fd632 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -23,21 +23,19 @@ Import le_upd_if.
 Inductive has_lc := HasLc | HasNoLc.
 
 Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
-  invGpreS_wsat : wsatGpreS Σ;
-  invGpreS_lc : lcGpreS Σ;
+  #[local] invGpreS_wsat :: wsatGpreS Σ;
+  #[local] invGpreS_lc :: lcGpreS Σ;
 }.
 
+(* [invGS_lc] needs to be global in order to enable the use of lemmas like
+[lc_split] that require [lcGS], and not [invGS]. [invGS_wsat] also needs to be
+global as the lemmas in [invariants.v] require it. *)
 Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
-  invGS_wsat : wsatGS Σ;
-  invGS_lc : lcGS Σ;
+  #[global] invGS_wsat :: wsatGS Σ;
+  #[global] invGS_lc :: lcGS Σ;
 }.
 Global Hint Mode invGS_gen - - : typeclass_instances.
 Global Hint Mode invGpreS - : typeclass_instances.
-Local Existing Instances invGpreS_wsat invGpreS_lc.
-(* [invGS_lc] needs to be global in order to enable the use of lemmas like [lc_split]
-   that require [lcGS], and not [invGS].
-   [invGS_wsat] also needs to be global as the lemmas in [invariants.v] require it. *)
-Global Existing Instances invGS_lc invGS_wsat.
 
 Notation invGS := (invGS_gen HasLc).
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 680d6c7ff5a02131456ba998f84e3a183fc52ea8..300cf7db6453637a002f4036eb5d6d2b40f93252 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -66,18 +66,16 @@ 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));
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_meta :: ghost_mapG Σ L gname;
+  #[local] 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 Σ;
+  #[local] 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 0914188548444b86fac42e17c4ebeade8685a918..7923ffd122800b0ef8938bc42112f0ea595dfb4d 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -31,15 +31,13 @@ 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))
+  #[local] 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 Σ;
+  #[local] 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 0029959c937081a231ea2adfe32e2f974d48308b..d1dd18258efc6bbc21c207376d142c15b45db2f5 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -12,9 +12,8 @@ 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 (agreeR (leibnizO V)));
+  #[local] ghost_map_inG :: inG Σ (gmap_viewR K (agreeR (leibnizO V)));
 }.
-Local Existing Instance ghost_map_inG.
 
 Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
   #[ GFunctor (gmap_viewR K (agreeR (leibnizO V))) ].
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 99864cb9deaf06bc3219b62055f86b7aa20ef852..ad9afd26a5d9f406da04f1efc1346fba970d17c7 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -8,9 +8,8 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class ghost_varG Σ (A : Type) := GhostVarG {
-  ghost_var_inG : inG Σ (dfrac_agreeR $ leibnizO A);
+  #[local] 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 a384b50d11235b45e0869c941bc0a4ef837cffb6..cdffbea6505307b3add885baeeb0b1d12266ca76 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -28,8 +28,7 @@ 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); }.
-Local Existing Instance gset_bijG_inG.
+  GsetBijG { #[local] gset_bijG_inG :: inG Σ (gset_bijR A B); }.
 Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 7d424f4a93cbf929235ff83a8cec8cb20e70ea54..bcc7f3311bdf06f5a7d5d07687092854af340dcf 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -10,15 +10,14 @@ Import uPred.
 
 (** The ghost state for later credits *)
 Class lcGpreS (Σ : gFunctors) := LcGpreS {
-  lcGpreS_inG : inG Σ (authR natUR)
+  #[local] lcGpreS_inG :: inG Σ (authR natUR)
 }.
 
 Class lcGS (Σ : gFunctors) := LcGS {
-  lcGS_inG : inG Σ (authR natUR);
+  #[local] lcGS_inG :: inG Σ (authR natUR);
   lcGS_name : gname;
 }.
 Global Hint Mode lcGS - : typeclass_instances.
-Local Existing Instances lcGS_inG lcGpreS_inG.
 
 Definition lcΣ := #[GFunctor (authR (natUR))].
 Global Instance subG_lcΣ {Σ} : subG lcΣ Σ → lcGpreS Σ.
diff --git a/iris/base_logic/lib/mono_Z.v b/iris/base_logic/lib/mono_Z.v
index 22a9e5a9c059fbffa87a2ac8b5d0be42c09bf850..d5dab1cc0acc73617551ac2e3f035da868ee7d8b 100644
--- a/iris/base_logic/lib/mono_Z.v
+++ b/iris/base_logic/lib/mono_Z.v
@@ -25,8 +25,7 @@ From iris.prelude Require Import options.
 Local Open Scope Z_scope.
 
 Class mono_ZG Σ :=
-  MonoZG { mono_ZG_natG : mono_natG Σ; }.
-Local Existing Instance mono_ZG_natG.
+  MonoZG { #[local] mono_ZG_natG :: mono_natG Σ; }.
 Definition mono_ZΣ := mono_natΣ.
 
 Local Definition mono_Z_auth_own_def `{!mono_ZG Σ}
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index c3def25f03e3a262f8a40abd4901dbeee7b0a63f..70ee37269959bf9dc8a04c4c93a435cdff5874b0 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -14,8 +14,7 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 Class mono_natG Σ :=
-  MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
-Local Existing Instance mono_natG_inG.
+  MonoNatG { #[local] mono_natG_inG :: inG Σ mono_natR; }.
 
 Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
 Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index d040790dd1942b5ceb3905720cd805e185457472..9f29cd4fd0d1d1ddc7eee8437edc2a0d0d237df9 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -9,8 +9,7 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inv_inG : inG Σ (prodR coPset_disjR (gset_disjR positive)).
-Local Existing Instance na_inv_inG.
+  #[local] na_inv_inG :: inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Definition na_invΣ : gFunctors :=
   #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 704561d969560e082e06d25b005a34d4f8810160..e23196d32620f187bc147138e0547d3a6c3c2629 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -9,16 +9,14 @@ 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)
+  #[local] 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 Σ;
+  #[local] 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 5ec788a6c234f9d72238f15c334b5dd7e5311860..076997ec43bbf05e0ab35b99e341687026be8d92 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -10,10 +10,9 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG : inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
+  #[local] saved_anything_inG :: inG Σ (dfrac_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 (dfrac_agreeRF F) ].
diff --git a/iris/base_logic/lib/token.v b/iris/base_logic/lib/token.v
index 7c1be9d55e38fe0367af2cd7c50f2d8b74cc0fd7..7df8631f7646c0ba94e7b3444043034bf757719b 100644
--- a/iris/base_logic/lib/token.v
+++ b/iris/base_logic/lib/token.v
@@ -8,9 +8,8 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class tokenG Σ := TokenG {
-  token_inG : inG Σ (exclR unitO);
+  #[local] token_inG :: inG Σ (exclR unitO);
 }.
-Local Existing Instance token_inG.
 Global Hint Mode tokenG - : typeclass_instances.
 
 Definition tokenΣ : gFunctors :=
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 44ae897befc57a505f23852132bc64cb99b3d8ff..82f822fa06311db16dc3f419b478004ca2a42fa4 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -31,6 +31,9 @@ Module wsatGS.
   Proof. solve_inG. Qed.
 End wsatGS.
 Import wsatGS.
+
+(* Make the instances local to this file. We cannot use #[local] in the code
+above, as that would make the instances local to the module. *)
 Local Existing Instances wsat_inG wsatGpreS_inv wsatGpreS_enabled wsatGpreS_disabled.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 11c858928af623c7ad6d333bf9d888a914307e25..7acca3e5f870f9cf63cacc0903b42ba65030816e 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -16,10 +16,9 @@ union.
 
 Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
   ownP_invG : invGS Σ;
-  ownP_inG : inG Σ (excl_authR (stateO Λ));
+  #[local] ownP_inG :: inG Σ (excl_authR (stateO Λ));
   ownP_name : gname;
 }.
-Local Existing Instance ownP_inG.
 
 Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
   iris_invGS := ownP_invG;
@@ -36,9 +35,8 @@ Definition ownPΣ (Λ : language) : gFunctors :=
 
 Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
   #[global] ownPPre_invG :: invGpreS Σ;
-  ownPPre_state_inG : inG Σ (excl_authR (stateO Λ))
+  #[local] 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 abc3996523ea293da16a5ebd6b6199ba7bcbc31b..7788aa4c7a4639144b6637c99ed26c4dee97e698 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -11,10 +11,9 @@ Import uPred.
 
 (* The CMRA we need. *)
 Class authG Σ (A : ucmra) := AuthG {
-  auth_inG : inG Σ (authR A);
+  #[local] auth_inG :: inG Σ (authR A);
   #[global] auth_cmra_discrete :: CmraDiscrete A;
 }.
-Local Existing Instance auth_inG.
 
 Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
 
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index e6317ab4db802afd2bceb5f3c5cfd5515fd52bee..5239ea0e24b9d5c2b86e51bbf6282db093b709d4 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -10,10 +10,9 @@ Import uPred.
 
 (** The CMRA we need. *)
 Class stsG Σ (sts : stsT) := StsG {
-  sts_inG : inG Σ (sts_resR sts);
+  #[local] sts_inG :: inG Σ (sts_resR sts);
   #[global] 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 f32bd01b31f5b722ac6e557d49e0c8501a0cee78..05232b2a28b6c9c5c0b92b34157061108a79290b 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -13,8 +13,8 @@ Definition incr : val := rec: "incr" "l" :=
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
-Class mcounterG Σ := MCounterG { mcounter_inG : inG Σ (authR max_natUR) }.
-Local Existing Instance mcounter_inG.
+Class mcounterG Σ :=
+  MCounterG { #[local] mcounter_inG :: inG Σ (authR max_natUR) }.
 
 Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
@@ -88,8 +88,7 @@ End mono_proof.
 
 (** Counter with contributions *)
 Class ccounterG Σ :=
-  CCounterG { ccounter_inG : inG Σ (frac_authR natR) }.
-Local Existing Instance ccounter_inG.
+  CCounterG { #[local] ccounter_inG :: inG Σ (frac_authR natR) }.
 
 Definition ccounterΣ : gFunctors :=
   #[GFunctor (frac_authR natR)].
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 61ed4eb431156d579898518e05aac8e0d5ed7347..e9ed87b27fe80a67ed52064831890ae948caa0a8 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -18,8 +18,7 @@ From iris.prelude Require Import options.
 
 Inductive state := Free | Locked.
 
-Class alockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
-Local Existing Instance lock_tokG.
+Class alockG Σ := LockG { #[local] lock_tokG :: ghost_varG Σ state }.
 Definition alockΣ : gFunctors := #[ghost_varΣ state].
 Global Instance subG_alockΣ {Σ} : subG alockΣ Σ → alockG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
index a801637ff506de96739f24859d5595b46458e954..d6de6ce032b28365badc1469a45aec736f2b60e5 100644
--- a/iris_heap_lang/lib/rw_spin_lock.v
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -31,8 +31,8 @@ Local Definition acquire_writer : val :=
 Local Definition release_writer : val :=
   λ: "l", "l" <- #0.
 
-Class rw_spin_lockG Σ := RwLockG { rwlock_tokG : inG Σ (authR (gmultisetUR Qp)) }.
-Local Existing Instance rwlock_tokG.
+Class rw_spin_lockG Σ :=
+  RwLockG { #[local] rwlock_tokG :: inG Σ (authR (gmultisetUR Qp)) }.
 
 Definition rw_spin_lockΣ : gFunctors := #[GFunctor (authR (gmultisetUR Qp)) ].
 Global Instance subG_rw_spin_lockΣ {Σ} : subG rw_spin_lockΣ Σ → rw_spin_lockG Σ.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 0d5fea58c918e521d8bec9f891b24b7475691889..b1ec3917b4b07f267e155fe8158be6cf95a4ea6d 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -19,8 +19,7 @@ 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) }.
-Local Existing Instance spawn_tokG.
+Class spawnG Σ := SpawnG { #[local] spawn_tokG :: inG Σ (exclR unitO) }.
 
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index f40495d33da91a293e4d90f2674d228c72fa4a0b..e3ea84d40535f6b9287e5746d3456f124101276d 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -13,8 +13,7 @@ Local Definition acquire : val :=
 Local Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
-Class spin_lockG Σ := LockG { lock_tokG : tokenG Σ }.
-Local Existing Instance lock_tokG.
+Class spin_lockG Σ := LockG { #[local] lock_tokG :: tokenG Σ }.
 
 Definition spin_lockΣ : gFunctors := #[tokenΣ].
 
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 416a3f514ce5e5ea4bd437d47b8fa9f46b11b97c..99c2bca846b2caa4eca68138b3853c2e06939ba4 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -28,8 +28,8 @@ Local Definition release : val :=
 
 (** The CMRAs we need. *)
 Class tlockG Σ :=
-  tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
-Local Existing Instance tlock_G.
+  #[local] tlock_G ::
+    inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
 
 Definition tlockΣ : gFunctors :=
   #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
diff --git a/iris_unstable/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
index e5422581a144b907e326f940d9c71354ff0fdce9..bb8df0b4b5c1db7843a25e3309e9bb8adf8fa3df 100644
--- a/iris_unstable/base_logic/mono_list.v
+++ b/iris_unstable/base_logic/mono_list.v
@@ -22,8 +22,7 @@ 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)) }.
-Local Existing Instance mono_list_inG.
+  MonoListG { #[local] mono_list_inG :: inG Σ (mono_listR (leibnizO A)) }.
 
 Definition mono_listΣ (A : Type) : gFunctors :=
   #[GFunctor (mono_listR (leibnizO A))].
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 7e247e3bd74499a0abe945860cccdc79bd72b47d..b8acd7e9a583aec8cbcf7f3c06e72016383106f3 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -174,8 +174,7 @@ Section M.
   Qed.
 End M.
 
-Class counterG Σ := CounterG { counter_tokG : inG Σ M_UR }.
-Local Existing Instance counter_tokG.
+Class counterG Σ := CounterG { #[local] counter_tokG :: inG Σ M_UR }.
 
 Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
 Global Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index aae8557e32b8dae84a0c6b74d0160f24cb2143a8..32dca58e8329e64a3383b2a8769ffa23d9ba2d76 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -31,8 +31,7 @@ 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 }.
-Local Existing Instance one_shot_inG.
+Class one_shotG Σ := { #[local] one_shot_inG :: inG Σ one_shotR }.
 
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index a27781f02722a224457889a09f36d5622ff23c60..f2a08c82202ea9b4fd41f6e8933a71b18da794b2 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -27,8 +27,7 @@ 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 }.
-Local Existing Instance one_shot_inG.
+Class one_shotG Σ := { #[local] one_shot_inG :: inG Σ one_shotR }.
 
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.