Also hide ghost_mapG instances

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;

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 Σ;

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 Σ;