reuse PreG class in G class where possible

iris/base_logic/lib/gen_inv_heap.v

@@ -30,17 +30,17 @@ Definition to_inv_heap {L V : Type} `{Countable L}
     (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
   prod_map (λ x, Excl' x) to_agree <$> h.
 
+Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
+}.
+
 Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
-  inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
+  inv_heap_inG :> inv_heapPreG L V Σ;
   inv_heap_name : gname
 }.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
 Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 
-Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
-}.
-
 Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
   #[ GFunctor (authR (inv_heap_mapUR L V)) ].
 

iris/base_logic/lib/proph_map.v

@@ -8,15 +8,15 @@ Local Notation proph_map P V := (gmap P (list V)).
 Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
+Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
+  { proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
+
 Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V));
+  proph_map_inG :> proph_mapPreG P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
 
-Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
-  { proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
-
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
 

iris/base_logic/lib/wsat.v

@@ -8,10 +8,14 @@ From iris.prelude Require Import options.
 exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
+  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
+    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    enabled_inPreG :> inG Σ coPset_disjR;
+    disabled_inPreG :> inG Σ (gset_disjR positive);
+  }.
+
   Class invG (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inG :> inG Σ coPset_disjR;
-    disabled_inG :> inG Σ (gset_disjR positive);
+    inv_inG :> invPreG Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
@@ -22,12 +26,6 @@ Module invG.
       GFunctor coPset_disjR;
       GFunctor (gset_disjR positive)].
 
-  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inPreG :> inG Σ coPset_disjR;
-    disabled_inPreG :> inG Σ (gset_disjR positive);
-  }.
-
   Global Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
   Proof. solve_inG. Qed.
 End invG.
@@ -192,7 +190,7 @@ Proof.
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  iModIntro; iExists (WsatG _ _ γI γE γD).
   rewrite /wsat /ownE -lock; iFrame.
   iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.