From 43853fc3c37ba6b6dbba45869bfaac60a952a2fe Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 Jan 2021 12:00:07 +0100
Subject: [PATCH] apply reveiw feedback

---
 iris/base_logic/lib/proph_map.v | 5 +++--
 iris/base_logic/lib/wsat.v      | 6 +++---
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index ba401e7db..fbed2c8b5 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -8,8 +8,9 @@ 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_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 :> proph_mapPreG P V Σ;
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 77e391a49..37ddb62df 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -8,13 +8,13 @@ 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 {
+  Class invPreG (Σ : gFunctors) : Set := InvPreG {
     inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
     enabled_inPreG :> inG Σ coPset_disjR;
     disabled_inPreG :> inG Σ (gset_disjR positive);
   }.
 
-  Class invG (Σ : gFunctors) : Set := WsatG {
+  Class invG (Σ : gFunctors) : Set := InvG {
     inv_inG :> invPreG Σ;
     invariant_name : gname;
     enabled_name : gname;
@@ -190,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 (InvG _ _ γI γE γD).
   rewrite /wsat /ownE -lock; iFrame.
   iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.
-- 
GitLab