From dbe95c90b91ca883a7a27f6ecd78b57c673bfebe Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 17 Mar 2022 12:38:09 +0100
Subject: [PATCH] Also hide ghost_mapG instances

---
 docs/resource_algebras.md       | 3 ++-
 iris/base_logic/lib/gen_heap.v  | 6 +++---
 iris/base_logic/lib/proph_map.v | 3 ++-
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 55c472ae6..2120a5897 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 9a41a34bb..97094a84d 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 98693dd34..762454424 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 Σ;
-- 
GitLab