From 55cd1cc954a27c906ecf18819e785c806afc8e05 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 31 Aug 2021 20:05:42 -0400
Subject: [PATCH] more consistent names for some class projections

---
 iris/program_logic/adequacy.v   |  2 +-
 iris/program_logic/ownp.v       |  4 ++--
 iris/program_logic/weakestpre.v |  4 ++--
 iris_heap_lang/primitive_laws.v | 12 ++++++------
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index e26604eaa..23fbdff87 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -219,7 +219,7 @@ Qed.
 (** This simpler form of adequacy requires the [irisGS] instance that you use
 everywhere to syntactically be of the form
 {|
-  iris_invG := ...;
+  iris_invGS := ...;
   state_interp σ _ κs _ := ...;
   fork_post v := ...;
   num_laters_per_step _ := 0;
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index ef838305f..859d05348 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -21,13 +21,13 @@ Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
 }.
 
 Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
-  iris_invG := ownP_invG;
+  iris_invGS := ownP_invG;
   state_interp σ _ κs _ := own ownP_name (●E σ)%I;
   fork_post _ := True%I;
   num_laters_per_step _ := 0;
   state_interp_mono _ _ _ _ := fupd_intro _ _
 }.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Definition ownPΣ (Λ : language) : gFunctors :=
   #[invΣ;
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index db92ff28d..b918c2933 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invG :> invGS Σ;
+  iris_invGS :> invGS Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [Λstate] is the global state,
@@ -45,7 +45,7 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
   state_interp_mono σ ns κs nt:
     state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
 }.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index e70d0ff1d..0af58af23 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -11,14 +11,14 @@ From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
 
 Class heapGS Σ := HeapGS {
-  heapG_invG : invGS Σ;
-  heapG_gen_heapG :> gen_heapGS loc (option val) Σ;
-  heapG_inv_heapG :> inv_heapGS loc (option val) Σ;
-  heapG_proph_mapG :> proph_mapGS proph_id (val * val) Σ;
+  heapGS_invGS : invGS Σ;
+  heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
+  heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
+  heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
 }.
 
-Global Instance heapG_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
-  iris_invG := heapG_invG;
+Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
+  iris_invGS := heapGS_invGS;
   state_interp σ _ κs _ :=
     (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
   fork_post _ := True%I;
-- 
GitLab