diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 2120a5897eb16623e8304de6f1c227a4473a4fef..1699a15f55cd84ce67b478b2fc32d03c069a8b6c 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -123,9 +123,10 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
 }.
 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 Instance 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
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 97094a84da18dd9d78928a5db973e814a8fdd0a5..7aa2d54cb74ad1f40584d6117ad028c87672b353 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -73,10 +73,11 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
 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 6545e873063aed86e2b54ddd9852c1c0b6cef948..127ae29235bb2b19e55a2c8b233b0b57e026a6db 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -36,9 +36,10 @@ Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
 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/proph_map.v b/iris/base_logic/lib/proph_map.v
index 762454424a4675431694123fc31b1fca1627d2d8..f405fa14fa3ebc9b1299dee9cf685472d3a6604b 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -14,10 +14,11 @@ Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
 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/wsat.v b/iris/base_logic/lib/wsat.v
index 93e6d4fcfabac379fc8ed6f26547939d5b9d2ebf..e6e9e1e81a35c33976725a24844bf35cb13228ab 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -15,7 +15,7 @@ Module invGS.
   }.
 
   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.