diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 55c472ae6a8d68a33045b0156bd24a5175b8257f..2120a5897eb16623e8304de6f1c227a4473a4fef 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -119,8 +119,9 @@ 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_name : gname;
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 9a41a34bb0b259e5e0eaa0e171b5c6edf3c9e1f7..97094a84da18dd9d78928a5db973e814a8fdd0a5 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -66,11 +66,11 @@ 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_heap : ghost_mapG Σ L V;
+  gen_heapGpreS_meta : ghost_mapG Σ L gname;
   gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
 }.
-Local Existing Instance gen_heapGpreS_meta_data.
+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 Σ;
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 98693dd34c62fe96599fb5f02f3aa857ada4cdd7..762454424a4675431694123fc31b1fca1627d2d8 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -9,8 +9,9 @@ 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 Σ;