From cabdcfc33e295439249f543d969531c93f730931 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 17 Mar 2022 14:03:39 +0100
Subject: [PATCH] Hide preG instances

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

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 2120a5897..1699a15f5 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 97094a84d..7aa2d54cb 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 6545e8730..127ae2923 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 762454424..f405fa14f 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 93e6d4fcf..e6e9e1e81 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.
-- 
GitLab