From 1118f70fe9890ab91d1985b9529abfb43fef9a38 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 May 2021 18:10:06 +0200
Subject: [PATCH] rename global singletons to 'GS' suffix

---
 CHANGELOG.md                                |  6 ++++
 docs/proof_guide.md                         |  2 ++
 iris/base_logic/lib/boxes.v                 |  4 +--
 iris/base_logic/lib/cancelable_invariants.v |  4 +--
 iris/base_logic/lib/fancy_updates.v         | 26 +++++++-------
 iris/base_logic/lib/gen_heap.v              | 38 ++++++++++-----------
 iris/base_logic/lib/gen_inv_heap.v          | 20 +++++------
 iris/base_logic/lib/invariants.v            |  4 +--
 iris/base_logic/lib/na_invariants.v         |  4 +--
 iris/base_logic/lib/proph_map.v             | 22 ++++++------
 iris/base_logic/lib/wsat.v                  | 34 +++++++++---------
 iris/program_logic/adequacy.v               | 22 ++++++------
 iris/program_logic/atomic.v                 |  4 +--
 iris/program_logic/ectx_lifting.v           |  2 +-
 iris/program_logic/lifting.v                |  2 +-
 iris/program_logic/ownp.v                   | 30 ++++++++--------
 iris/program_logic/total_adequacy.v         |  8 ++---
 iris/program_logic/total_ectx_lifting.v     |  2 +-
 iris/program_logic/total_lifting.v          |  2 +-
 iris/program_logic/total_weakestpre.v       | 16 ++++-----
 iris/program_logic/weakestpre.v             | 16 ++++-----
 iris_deprecated/base_logic/auth.v           |  4 +--
 iris_deprecated/base_logic/sts.v            | 10 +++---
 iris_deprecated/base_logic/viewshifts.v     |  4 +--
 iris_deprecated/program_logic/hoare.v       |  4 +--
 iris_heap_lang/adequacy.v                   | 18 +++++-----
 iris_heap_lang/derived_laws.v               |  4 +--
 iris_heap_lang/lib/arith.v                  |  8 ++---
 iris_heap_lang/lib/array.v                  |  2 +-
 iris_heap_lang/lib/assert.v                 |  4 +--
 iris_heap_lang/lib/atomic_heap.v            |  8 ++---
 iris_heap_lang/lib/clairvoyant_coin.v       |  2 +-
 iris_heap_lang/lib/counter.v                |  4 +--
 iris_heap_lang/lib/diverge.v                |  2 +-
 iris_heap_lang/lib/increment.v              |  6 ++--
 iris_heap_lang/lib/lazy_coin.v              |  2 +-
 iris_heap_lang/lib/lock.v                   |  4 +--
 iris_heap_lang/lib/nondet_bool.v            |  2 +-
 iris_heap_lang/lib/par.v                    |  2 +-
 iris_heap_lang/lib/spawn.v                  |  4 +--
 iris_heap_lang/lib/spin_lock.v              |  6 ++--
 iris_heap_lang/lib/ticket_lock.v            |  4 +--
 iris_heap_lang/primitive_laws.v             | 16 ++++-----
 iris_heap_lang/proofmode.v                  | 22 ++++++------
 iris_heap_lang/total_adequacy.v             |  6 ++--
 tests/algebra.v                             |  2 +-
 tests/atomic.v                              |  6 ++--
 tests/heap_lang.v                           | 12 +++----
 tests/heap_lang2.v                          |  2 +-
 tests/heap_lang_proph.v                     |  2 +-
 tests/ipm_paper.v                           |  6 ++--
 tests/iris_notation.v                       |  2 +-
 tests/list_reverse.v                        |  2 +-
 tests/one_shot.v                            |  4 +--
 tests/one_shot_once.v                       |  4 +--
 tests/proofmode_ascii.v                     |  4 +--
 tests/proofmode_iris.v                      |  4 +--
 tests/proofmode_monpred.v                   |  2 +-
 tests/tree_sum.v                            |  6 ++--
 59 files changed, 241 insertions(+), 233 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d798d12a5..f93680cbf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -64,6 +64,9 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
   It applies even if invariants stay open accross an arbitrary number of laters.
   (by Jacques-Henri Jourdan)
+* Rename those `*G` typeclasses that must be global singletons to `*GS`, and
+  their corresponding `preG` class to `GpreS`. Affects `invG`, `irisG`,
+  `gen_heapG`, `inv_heapG`, `proph_mapG`, `ownPG`, `heapG`.
 
 **Changes in `program_logic`:**
 
@@ -105,6 +108,9 @@ s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 s/\bbig_sep(L|L2|M|M2|S)_intuitionistically_forall\b/big_sep\1_intro/g
 s/\bbig_orL_lookup\b/big_orL_intro/g
 s/\bbupd_forall\b/bupd_plain_forall/g
+# "global singleton" rename
+s/\b(inv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)G\b/\1GS/g
+s/\b([iI]nv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)PreG\b/\1GpreS/g
 EOF
 ```
 
diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index e97efd204..59ab9118a 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -216,6 +216,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
 * G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
+* GS: global singleton (a `*G` typeclass withe extra data that needs to be unique in a proof)
+* GpreS: collecting preconditions to instantiate the corresponding `*GS`
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)
 * T: canonical structures for algebraic classes (for example ofe for OFEs, cmra for cameras)
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index ca565ab8c..68ac12c24 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -17,7 +17,7 @@ Global Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.
-  Context `{!invG Σ, !boxG Σ} (N : namespace).
+  Context `{!invGS Σ, !boxG Σ} (N : namespace).
 
   Definition slice_name := gname.
 
@@ -46,7 +46,7 @@ Global Instance: Params (@slice) 5 := {}.
 Global Instance: Params (@box) 5 := {}.
 
 Section box.
-Context `{!invG Σ, !boxG Σ} (N : namespace).
+Context `{!invGS Σ, !boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index c74b89b63..88b0cda57 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -12,7 +12,7 @@ Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{!invG Σ, !cinvG Σ}.
+  Context `{!invGS Σ, !cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -23,7 +23,7 @@ End defs.
 Global Instance: Params (@cinv) 5 := {}.
 
 Section proofs.
-  Context `{!invG Σ, !cinvG Σ}.
+  Context `{!invGS Σ, !cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index c7d7a4050..3feb1b40c 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -4,18 +4,18 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
 From iris.prelude Require Import options.
-Export invG.
+Export invGS.
 Import uPred.
 
-Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
 Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
 Global Arguments uPred_fupd {Σ _}.
-Lemma uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Lemma uPred_fupd_eq `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
-Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{!invGS Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
 Proof.
   split.
   - rewrite uPred_fupd_eq. solve_proper.
@@ -33,13 +33,13 @@ Proof.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
 Qed.
-Global Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+Global Instance uPred_bi_fupd `{!invGS Σ} : BiFUpd (uPredI (iResUR Σ)) :=
   {| bi_fupd_mixin := uPred_fupd_mixin |}.
 
-Global Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Global Instance uPred_bi_bupd_fupd `{!invGS Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
 Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
 
-Global Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_plainly `{!invGS Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
 Proof.
   split.
   - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
@@ -60,8 +60,8 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
-  (∀ `{Hinv: !invG Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
+Lemma fupd_plain_soundness `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
+  (∀ `{Hinv: !invGS Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
@@ -70,8 +70,8 @@ Proof.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness `{!invGpreS Σ} φ n :
+  (∀ `{Hinv: !invGS Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
@@ -84,8 +84,8 @@ Proof.
   iNext. iMod "H" as %Hφ. auto.
 Qed.
 
-Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness' `{!invGpreS Σ} φ n :
+  (∀ `{Hinv: !invGS Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n)=>Hinv. destruct n as [|n].
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 005a01456..a0a086c8d 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -11,7 +11,7 @@ Import uPred.
 (** This file provides a generic mechanism for a language-level point-to
 connective [l ↦{dq} v] reflecting the physical heap.  This library is designed to
 be used as a singleton (i.e., with only a single instance existing in any
-proof), with the [gen_heapG] typeclass providing the ghost names of that unique
+proof), with the [gen_heapGS] typeclass providing the ghost names of that unique
 instance.  That way, [mapsto] does not need an explicit [gname] parameter.
 This mechanism can be plugged into a language and related to the physical heap
 by using [gen_heap_interp σ] in the state interpretation of the weakest
@@ -65,18 +65,18 @@ these can be matched up with the invariant namespaces. *)
 
 (** The CMRAs we need, and the global ghost names we are using. *)
 
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> ghost_mapG Σ L V;
-  gen_meta_preG_inG :> ghost_mapG Σ L gname;
-  gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
+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_meta_data :> inG Σ (reservation_mapR (agreeR positiveO));
 }.
 
-Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
-  gen_heap_inG :> gen_heapPreG L V Σ;
+Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
+  gen_heap_inG :> gen_heapGpreS L V Σ;
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
-Global Arguments GenHeapG L V Σ {_ _ _} _ _.
+Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
 Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
 Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
@@ -86,12 +86,12 @@ Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
   GFunctor (reservation_mapR (agreeR positiveO))
 ].
 
-Global Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
-  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
+Global Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
+  subG (gen_heapΣ L V) Σ → gen_heapGpreS L V Σ.
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{Countable L, hG : !gen_heapG L V Σ}.
+  Context `{Countable L, hG : !gen_heapGS L V Σ}.
 
   Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
     (* The [⊆] is used to avoid assigning ghost information to the locations in
@@ -135,7 +135,7 @@ Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
   (at level 20, format "l  ↦  v") : bi_scope.
 
 Section gen_heap.
-  Context {L V} `{Countable L, !gen_heapG L V Σ}.
+  Context {L V} `{Countable L, !gen_heapGS L V Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
@@ -290,28 +290,28 @@ End gen_heap.
 
 (** This variant of [gen_heap_init] should only be used when absolutely needed.
 The key difference to [gen_heap_init] is that the [inG] instances in the new
-[gen_heapG] instance are related to the original [gen_heapPreG] instance,
+[gen_heapGS] instance are related to the original [gen_heapGpreS] instance,
 whereas [gen_heap_init] forgets about that relation. *)
-Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init_names `{Countable L, !gen_heapGpreS L V Σ} σ :
   ⊢ |==> ∃ γh γm : gname,
-    let hG := GenHeapG L V Σ γh γm in
+    let hG := GenHeapGS L V Σ γh γm in
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
   iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
   iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
   iExists γh, γm.
-  iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
+  iAssert (gen_heap_interp (hG:=GenHeapGS _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
   { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
   iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
   { apply map_disjoint_empty_r. }
   rewrite right_id_L. done.
 Qed.
 
-Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ,
+Lemma gen_heap_init `{Countable L, !gen_heapGpreS L V Σ} σ :
+  ⊢ |==> ∃ _ : gen_heapGS L V Σ,
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
   iMod (gen_heap_init_names σ) as (γh γm) "Hinit".
-  iExists (GenHeapG _ _ _ γh γm).
+  iExists (GenHeapGS _ _ _ γh γm).
   done.
 Qed.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index ecb038af2..2e196fbd9 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -30,12 +30,12 @@ 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_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  inv_heapGpreS_inG :> inG Σ (authR (inv_heap_mapUR L V))
 }.
 
-Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
-  inv_heap_inG :> inv_heapPreG L V Σ;
+Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
+  inv_heap_inG :> inv_heapGpreS L V Σ;
   inv_heap_name : gname
 }.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
@@ -44,13 +44,13 @@ Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
   #[ GFunctor (authR (inv_heap_mapUR L V)) ].
 
-Global Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
-  subG (inv_heapΣ L V) Σ → inv_heapPreG L V Σ.
+Global Instance subG_inv_heapGpreS (L V : Type) `{Countable L} {Σ} :
+  subG (inv_heapΣ L V) Σ → inv_heapGpreS L V Σ.
 Proof. solve_inG. Qed.
 
 Section definitions.
   Context {L V : Type} `{Countable L}.
-  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
+  Context `{!invGS Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
 
   Definition inv_heap_inv_P : iProp Σ :=
     ∃ h : gmap L (V * (V -d> PropO)),
@@ -112,8 +112,8 @@ Section to_inv_heap.
   Qed.
 End to_inv_heap.
 
-Lemma inv_heap_init (L V : Type) `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E :
-  ⊢ |==> ∃ _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
+Lemma inv_heap_init (L V : Type) `{Countable L, !invGS Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
+  ⊢ |==> ∃ _ : inv_heapGS L V Σ, |={E}=> inv_heap_inv L V.
 Proof.
   iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
   { rewrite auth_auth_valid. exact: to_inv_heap_valid. }
@@ -126,7 +126,7 @@ Qed.
 
 Section inv_heap.
   Context {L V : Type} `{Countable L}.
-  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
+  Context `{!invGS Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
   Implicit Types (l : L) (v : V) (I : V → Prop).
   Implicit Types (h : gmap L (V * (V -d> PropO))).
 
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index 91f87d5de..620c5994e 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 (** Semantic Invariants *)
-Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{!invGS Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv := inv_aux.(unseal).
@@ -17,7 +17,7 @@ Global Instance: Params (@inv) 3 := {}.
 
 (** * Invariants *)
 Section inv.
-  Context `{!invG Σ}.
+  Context `{!invGS Σ}.
   Implicit Types i : positive.
   Implicit Types N : namespace.
   Implicit Types E : coPset.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index d4858462d..1f44bab6e 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -16,7 +16,7 @@ Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{!invG Σ, !na_invG Σ}.
+  Context `{!invGS Σ, !na_invG Σ}.
 
   Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
     own p (CoPset E, GSet ∅).
@@ -30,7 +30,7 @@ Global Instance: Params (@na_inv) 3 := {}.
 Typeclasses Opaque na_own na_inv.
 
 Section proofs.
-  Context `{!invG Σ, !na_invG Σ}.
+  Context `{!invGS Σ, !na_invG Σ}.
 
   Global Instance na_own_timeless p E : Timeless (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 121e42e62..44d78abe6 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -8,12 +8,12 @@ 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 :> ghost_mapG Σ P (list V)
+Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
+  proph_map_GpreS_inG :> ghost_mapG Σ P (list V)
 }.
 
-Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> proph_mapPreG P V Σ;
+Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
+  proph_map_inG :> proph_mapGpreS P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
@@ -21,12 +21,12 @@ Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[ghost_mapΣ P (list V)].
 
-Global Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
-  subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
+Global Instance subG_proph_mapGpreS {Σ P V} `{Countable P} :
+  subG (proph_mapΣ P V) Σ → proph_mapGpreS P V Σ.
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{pG : proph_mapG P V Σ}.
+  Context `{pG : proph_mapGS P V Σ}.
   Implicit Types pvs : proph_val_list P V.
   Implicit Types R : proph_map P V.
   Implicit Types p : P.
@@ -72,16 +72,16 @@ Section list_resolves.
   Qed.
 End list_resolves.
 
-Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
-  ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_interp pvs ps.
+Lemma proph_map_init `{Countable P, !proph_mapGpreS P V PVS} pvs ps :
+  ⊢ |==> ∃ _ : proph_mapGS P V PVS, proph_map_interp pvs ps.
 Proof.
   iMod (ghost_map_alloc_empty) as (γ) "Hh".
-  iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
+  iModIntro. iExists (ProphMapGS P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. done.
 Qed.
 
 Section proph_map.
-  Context `{proph_mapG P V Σ}.
+  Context `{proph_mapGS P V Σ}.
   Implicit Types p : P.
   Implicit Types v : V.
   Implicit Types vs : list V.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index bbfc5a9e9..fd6546c97 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -5,17 +5,17 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 (** All definitions in this file are internal to [fancy_updates] with the
-exception of what's in the [invG] module. The module [invG] is thus exported in
+exception of what's in the [invGS] module. The module [invGS] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
-Module invG.
-  Class invPreG (Σ : gFunctors) : Set := InvPreG {
-    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inPreG :> inG Σ coPset_disjR;
-    disabled_inPreG :> inG Σ (gset_disjR positive);
+Module invGS.
+  Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
+    invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    invGpreS_enabled :> inG Σ coPset_disjR;
+    invGpreS_disabled :> inG Σ (gset_disjR positive);
   }.
 
-  Class invG (Σ : gFunctors) : Set := InvG {
-    inv_inG :> invPreG Σ;
+  Class invGS (Σ : gFunctors) : Set := InvG {
+    inv_inG :> invGpreS Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
@@ -26,36 +26,36 @@ Module invG.
       GFunctor coPset_disjR;
       GFunctor (gset_disjR positive)].
 
-  Global Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+  Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
   Proof. solve_inG. Qed.
-End invG.
-Import invG.
+End invGS.
+Import invGS.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
-Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{!invGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
 Typeclasses Opaque ownI.
 Global Instance: Params (@invariant_unfold) 1 := {}.
 Global Instance: Params (@ownI) 3 := {}.
 
-Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{!invGS Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
 Global Instance: Params (@ownE) 3 := {}.
 
-Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{!invGS Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
 Global Instance: Params (@ownD) 3 := {}.
 
-Definition wsat `{!invG Σ} : iProp Σ :=
+Definition wsat `{!invGS Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
     own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
-Context `{!invG Σ}.
+Context `{!invGS Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
@@ -182,7 +182,7 @@ Qed.
 End wsat.
 
 (* Allocation of an initial world *)
-Lemma wsat_alloc `{!invPreG Σ} : ⊢ |==> ∃ _ : invG Σ, wsat ∗ ownE ⊤.
+Lemma wsat_alloc `{!invGpreS Σ} : ⊢ |==> ∃ _ : invGS Σ, wsat ∗ ownE ⊤.
 Proof.
   iIntros.
   iMod (own_alloc (gmap_view_auth 1 ∅)) as (γI) "HI";
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index d9340a5cc..2b06be13b 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -9,7 +9,7 @@ Import uPred.
 we prove a number of auxilary results. *)
 
 Section adequacy.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -117,9 +117,9 @@ Qed.
 End adequacy.
 
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
+Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 φ
         (num_laters_per_step : nat → nat) :
-  (∀ `{Hinv : !invG Σ},
+  (∀ `{Hinv : !invGS Σ},
     ⊢ |={⊤}=> ∃
          (s: stuckness)
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
@@ -128,7 +128,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
          (* Note: existentially quantifying over Iris goal! [iExists _] should
          usually work. *)
          state_interp_mono,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+       let _ : irisGS Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
                                   state_interp_mono
        in
        stateI σ1 0 κs 0 ∗
@@ -216,7 +216,7 @@ Proof.
   right; exists (t2' ++ e3 :: t2'' ++ efs), σ3, κ; econstructor; eauto.
 Qed.
 
-(** This simpler form of adequacy requires the [irisG] instance that you use
+(** This simpler form of adequacy requires the [irisGS] instance that you use
 everywhere to syntactically be of the form
 {|
   iris_invG := ...;
@@ -229,12 +229,12 @@ In other words, the state interpretation must ignore [ns] and [nt], the number
 of laters per step must be 0, and the proof of [state_interp_mono] must have
 this specific proof term.
 *)
-Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
-  (∀ `{Hinv : !invG Σ} κs,
+Corollary wp_adequacy Σ Λ `{!invGpreS Σ} s e σ φ :
+  (∀ `{Hinv : !invGS Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ :=
+       let _ : irisGS Λ Σ :=
            IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
                  (λ _ _ _ _, fupd_intro _ _)
        in
@@ -252,12 +252,12 @@ Proof.
   iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
 Qed.
 
-Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
-  (∀ `{Hinv : !invG Σ} κs,
+Corollary wp_invariance Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
+  (∀ `{Hinv : !invGS Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
+       let _ : irisGS Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
               (λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
        stateI σ1 κs 0 ∗ WP e1 @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝)) →
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index fead228df..97ea858a7 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
 example where we want it to be anything else. *)
-Definition atomic_wp `{!irisG Λ Σ} {TA TB : tele}
+Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
   (Eo : coPset) (* (outer) mask *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
@@ -95,7 +95,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
 
 (** Theory *)
 Section lemmas.
-  Context `{!irisG Λ Σ} {TA TB : tele}.
+  Context `{!irisGS Λ Σ} {TA TB : tele}.
   Notation iProp := (iProp Σ).
   Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
 
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 468b0bfa6..1dd14d2b2 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.prelude Require Import options.
 
 Section wp.
-Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisGS Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 1a5aaca96..edc7b8f81 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -6,7 +6,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 
 Section lifting.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index b160c1b62..60d7e4507 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -14,13 +14,13 @@ a more interesting notion of ownership, such as the standard heap with disjoint
 union.
 *)
 
-Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
-  ownP_invG : invG Σ;
+Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
+  ownP_invG : invGS Σ;
   ownP_inG :> inG Σ (excl_authR (stateO Λ));
   ownP_name : gname;
 }.
 
-Global Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
+Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
   iris_invG := ownP_invG;
   state_interp σ _ κs _ := own ownP_name (●E σ)%I;
   fork_post _ := True%I;
@@ -33,23 +33,23 @@ Definition ownPΣ (Λ : language) : gFunctors :=
   #[invΣ;
     GFunctor (excl_authR (stateO Λ))].
 
-Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
-  ownPPre_invG :> invPreG Σ;
+Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
+  ownPPre_invG :> invGpreS Σ;
   ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
 }.
 
-Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
+Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPGpreS Λ Σ.
 Proof. solve_inG. Qed.
 
 (** Ownership *)
-Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
+Definition ownP `{!ownPGS Λ Σ} (σ : state Λ) : iProp Σ :=
   own ownP_name (◯E σ).
 Typeclasses Opaque ownP.
 Global Instance: Params (@ownP) 3 := {}.
 
 (* Adequacy *)
-Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
-  (∀ `{!ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+Theorem ownP_adequacy Σ `{!ownPGpreS Λ Σ} s e σ φ :
+  (∀ `{!ownPGS Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
@@ -58,11 +58,11 @@ Proof.
     first by apply excl_auth_valid.
   iModIntro. iExists (λ σ κs, own γσ (●E σ))%I, (λ _, True%I).
   iFrame "Hσ".
-  iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
+  iApply (Hwp (OwnPGS _ _ _ _ γσ)). rewrite /ownP. iFrame.
 Qed.
 
-Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
-  (∀ `{!ownPG Λ Σ},
+Theorem ownP_invariance Σ `{!ownPGpreS Λ Σ} s e σ1 t2 σ2 φ :
+  (∀ `{!ownPGS Λ Σ},
       ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
       |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc erased_step ([e], σ1) (t2, σ2) →
@@ -74,7 +74,7 @@ Proof.
     first by apply auth_both_valid_discrete.
   iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
   iFrame "Hσ".
-  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
+  iMod (Hwp (OwnPGS _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
   iIntros "!> Hσ". iExists ∅. iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
   iDestruct (own_valid_2 with "Hσ Hσf")
@@ -84,7 +84,7 @@ Qed.
 
 (** Lifting *)
 Section lifting.
-  Context `{!ownPG Λ Σ}.
+  Context `{!ownPGS Λ Σ}.
   Implicit Types s : stuckness.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
@@ -209,7 +209,7 @@ End lifting.
 
 Section ectx_lifting.
   Import ectx_language.
-  Context {Λ : ectxLanguage} `{!ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
+  Context {Λ : ectxLanguage} `{!ownPGS Λ Σ} {Hinh : Inhabited (state Λ)}.
   Implicit Types s : stuckness.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index d1c470c58..ed100b2d8 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Section adequacy.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
@@ -116,12 +116,12 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
-  (∀ `{Hinv : !invG Σ},
+Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ :
+  (∀ `{Hinv : !invGS Σ},
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ :=
+       let _ : irisGS Λ Σ :=
            IrisG _ _ Hinv (λ σ _, stateI σ) fork_post (λ _, 0)
                  (λ _ _ _ _, fupd_intro _ _)
        in
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 35d776409..473b61acb 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ectx_language total_weakestpre total_lift
 From iris.prelude Require Import options.
 
 Section wp.
-Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisGS Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index 101bf4d62..aac06d858 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export total_weakestpre.
 From iris.prelude Require Import options.
 
 Section lifting.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 8b98e91ae..7ef86fa5b 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -8,7 +8,7 @@ Import uPred.
 definition of normal (i.e. partial) weakest precondition, with the exception
 that there is no later modality. Hence, instead of taking a Banach's fixpoint,
 we take a least fixpoint. *)
-Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
+Definition twp_pre `{!irisGS Λ Σ} (s : stuckness)
       (wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
@@ -25,7 +25,7 @@ Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
 
 (** This is some uninteresting bookkeeping to prove that [twp_pre_mono] is
 monotone. The actual least fixpoint [twp_def] can be found below. *)
-Lemma twp_pre_mono `{!irisG Λ Σ} s
+Lemma twp_pre_mono `{!irisGS Λ Σ} s
     (wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
   ⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
     ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ.
@@ -42,12 +42,12 @@ Proof.
 Qed.
 
 (* Uncurry [twp_pre] and equip its type with an OFE structure *)
-Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
+Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
   (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
   prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
     curry3 ∘ twp_pre s ∘ uncurry3.
 
-Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
+Local Instance twp_pre_mono' `{!irisGS Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
   - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
@@ -57,17 +57,17 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
+Definition twp_def `{!irisGS Λ Σ} : Twp Λ (iProp Σ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
 Global Arguments twp' {Λ Σ _}.
 Global Existing Instance twp'.
-Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
+Lemma twp_eq `{!irisGS Λ Σ} : twp = @twp_def Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
 Section twp.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -276,7 +276,7 @@ End twp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{!irisG Λ Σ}.
+  Context `{!irisGS Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index e3656a5dd..bb54d9962 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -7,8 +7,8 @@ From iris.bi Require Export weakestpre.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invG :> invG Σ;
+Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
+  iris_invG :> invGS Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [Λstate] is the global state,
@@ -47,7 +47,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
 }.
 Global Opaque iris_invG.
 
-Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
+Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
@@ -62,7 +62,7 @@ Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
-Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
+Local Instance wp_pre_contractive `{!irisGS Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
   do 24 (f_contractive || f_equiv).
@@ -73,17 +73,17 @@ Proof.
   - by rewrite -IH.
 Qed.
 
-Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
+Definition wp_def `{!irisGS Λ Σ} : Wp Λ (iProp Σ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
 Global Arguments wp' {Λ Σ _}.
 Global Existing Instance wp'.
-Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
+Lemma wp_eq `{!irisGS Λ Σ} : wp = @wp_def Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -358,7 +358,7 @@ End wp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{!irisG Λ Σ}.
+  Context `{!irisGS Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
diff --git a/iris_deprecated/base_logic/auth.v b/iris_deprecated/base_logic/auth.v
index 64b121384..451cf54e1 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -20,7 +20,7 @@ Global Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → aut
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{!invG Σ, !authG Σ A} {T : Type} (γ : gname).
+  Context `{!invGS Σ, !authG Σ A} {T : Type} (γ : gname).
 
   Definition auth_own (a : A) : iProp Σ :=
     own γ (◯ a).
@@ -64,7 +64,7 @@ Global Instance: Params (@auth_inv) 5 := {}.
 Global Instance: Params (@auth_ctx) 7 := {}.
 
 Section auth.
-  Context `{!invG Σ, !authG Σ A}.
+  Context `{!invGS Σ, !authG Σ A}.
   Context {T : Type} `{!Inhabited T}.
   Context (f : T → A) (φ : T → iProp Σ).
   Implicit Types N : namespace.
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index de1785235..fc9cd06c3 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -28,7 +28,7 @@ Section definitions.
     own γ (sts_frag_up s T).
   Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ :=
     ∃ s, own γ (sts_auth s ∅) ∗ φ s.
-  Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
+  Definition sts_ctx `{!invGS Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
     inv N (sts_inv φ).
 
   Global Instance sts_inv_ne n :
@@ -41,13 +41,13 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_ne `{!invG Σ} n N :
+  Global Instance sts_ctx_ne `{!invGS Σ} n N :
     Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_proper `{!invG Σ} N :
+  Global Instance sts_ctx_proper `{!invGS Σ} N :
     Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_persistent `{!invG Σ} N φ : Persistent (sts_ctx N φ).
+  Global Instance sts_ctx_persistent `{!invGS Σ} N φ : Persistent (sts_ctx N φ).
   Proof. apply _. Qed.
   Global Instance sts_own_persistent s : Persistent (sts_own s ∅).
   Proof. apply _. Qed.
@@ -61,7 +61,7 @@ Global Instance: Params (@sts_own) 5 := {}.
 Global Instance: Params (@sts_ctx) 6 := {}.
 
 Section sts.
-  Context `{!invG Σ, !stsG Σ sts}.
+  Context `{!invGS Σ, !stsG Σ sts}.
   Implicit Types φ : sts.state sts → iProp Σ.
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Σ.
diff --git a/iris_deprecated/base_logic/viewshifts.v b/iris_deprecated/base_logic/viewshifts.v
index c2a571e94..379bf4265 100644
--- a/iris_deprecated/base_logic/viewshifts.v
+++ b/iris_deprecated/base_logic/viewshifts.v
@@ -9,7 +9,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 
-Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs `{!invGS Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   □ (P -∗ |={E1,E2}=> Q).
 Global Arguments vs {_ _} _ _ _%I _%I.
 
@@ -29,7 +29,7 @@ Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
    format "P  ={ E }=>  Q") : stdpp_scope.
 
 Section vs.
-Context `{!invG Σ}.
+Context `{!invGS Σ}.
 Implicit Types P Q R : iProp Σ.
 Implicit Types N : namespace.
 
diff --git a/iris_deprecated/program_logic/hoare.v b/iris_deprecated/program_logic/hoare.v
index c40fa8df9..8ff987966 100644
--- a/iris_deprecated/program_logic/hoare.v
+++ b/iris_deprecated/program_logic/hoare.v
@@ -9,7 +9,7 @@ From iris.deprecated.base_logic Require Export viewshifts.
 From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 
-Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
+Definition ht `{!irisGS Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
   (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
 Global Instance: Params (@ht) 5 := {}.
@@ -47,7 +47,7 @@ Notation "{{ P } } e ? {{ v , Q } }" := (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
    format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
 
 Section hoare.
-Context `{!irisG Λ Σ}.
+Context `{!irisGS Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val Λ → iProp Σ.
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index d24fe5afd..3ce089fac 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -4,20 +4,20 @@ From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
-Class heapPreG Σ := HeapPreG {
-  heap_preG_iris :> invPreG Σ;
-  heap_preG_heap :> gen_heapPreG loc (option val) Σ;
-  heap_preG_inv_heap :> inv_heapPreG loc (option val) Σ;
-  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
+Class heapGpreS Σ := HeapGpreS {
+  heapGpreS_iris :> invGpreS Σ;
+  heapGpreS_heap :> gen_heapGpreS loc (option val) Σ;
+  heapGpreS_inv_heap :> inv_heapGpreS loc (option val) Σ;
+  heapGpreS_proph :> proph_mapGpreS proph_id (val * val) Σ;
 }.
 
 Definition heapΣ : gFunctors :=
   #[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val); proph_mapΣ proph_id (val * val)].
-Global Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Global Instance subG_heapGpreS {Σ} : subG heapΣ Σ → heapGpreS Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
-  (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
+  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (? κs) "".
@@ -27,5 +27,5 @@ Proof.
   iModIntro. iExists
     (λ σ κs, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
     (λ _, True%I).
-  iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
+  iFrame. iApply (Hwp (HeapGS _ _ _ _ _)). done.
 Qed.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 0a812eef8..66a870aa5 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -14,7 +14,7 @@ From iris.prelude Require Import options.
 (** The [array] connective is a version of [mapsto] that works
 with lists of values. *)
 
-Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
+Definition array `{!heapGS Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   [∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v.
 
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
@@ -33,7 +33,7 @@ Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
 lead to overlapping instances. *)
 
 Section lifting.
-Context `{!heapG Σ}.
+Context `{!heapGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types σ : state.
diff --git a/iris_heap_lang/lib/arith.v b/iris_heap_lang/lib/arith.v
index 8a2165ce6..17f037256 100644
--- a/iris_heap_lang/lib/arith.v
+++ b/iris_heap_lang/lib/arith.v
@@ -14,7 +14,7 @@ Definition minimum : val :=
 Definition maximum : val :=
   λ: "m" "n", if: "m" < "n" then "n" else "m".
 
-Lemma minimum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+Lemma minimum_spec `{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : Z) :
   ▷ Φ #(m `min` n) -∗
   WP minimum #m #n @ s;E {{ Φ }}.
 Proof.
@@ -23,12 +23,12 @@ Proof.
   - rewrite Z.min_r; [ done | by lia ].
 Qed.
 
-Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+Lemma minimum_spec_nat `{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : nat) :
   ▷ Φ #(m `min` n)%nat -∗
   WP minimum #m #n @ s;E {{ Φ }}.
 Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
 
-Lemma maximum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+Lemma maximum_spec `{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : Z) :
   ▷ Φ #(m `max` n) -∗
   WP maximum #m #n @ s;E {{ Φ }}.
 Proof.
@@ -37,7 +37,7 @@ Proof.
   - rewrite Z.max_l; [ done | by lia ].
 Qed.
 
-Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+Lemma maximum_spec_nat `{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : nat) :
   ▷ Φ #(m `max` n)%nat -∗
   WP maximum #m #n @ s;E {{ Φ }}.
 Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 86598a764..4508f0fef 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -50,7 +50,7 @@ Definition array_init : val :=
     "src".
 
 Section proof.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma twp_array_free s E l vs (n : Z) :
     n = length vs →
diff --git a/iris_heap_lang/lib/assert.v b/iris_heap_lang/lib/assert.v
index 160377bc0..a63b674ec 100644
--- a/iris_heap_lang/lib/assert.v
+++ b/iris_heap_lang/lib/assert.v
@@ -10,7 +10,7 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
 Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.
 
-Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma twp_assert `{!heapGS Σ} E (Φ : val → iProp Σ) e :
   WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
   WP (assert: e)%V @ E [{ Φ }].
 Proof.
@@ -18,7 +18,7 @@ Proof.
   wp_smart_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
-Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma wp_assert `{!heapGS Σ} E (Φ : val → iProp Σ) e :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
   WP (assert: e)%V @ E {{ Φ }}.
 Proof.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index c095508e8..302215a8a 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -6,7 +6,7 @@ From iris.heap_lang Require Import notation proofmode.
 From iris.prelude Require Import options.
 
 (** A general logically atomic interface for a heap. *)
-Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
+Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   free : val;
@@ -69,7 +69,7 @@ Module notation.
 End notation.
 
 Section derived.
-  Context `{!heapG Σ, !atomic_heap Σ}.
+  Context `{!heapGS Σ, !atomic_heap Σ}.
 
   Import notation.
 
@@ -99,7 +99,7 @@ Definition primitive_cmpxchg : val :=
   λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
 
 Section proof.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma primitive_alloc_spec (v : val) :
     {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
@@ -148,7 +148,7 @@ End proof.
 
 (* NOT an instance because users should choose explicitly to use it
      (using [Explicit Instance]). *)
-Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
+Definition primitive_atomic_heap `{!heapGS Σ} : atomic_heap Σ :=
   {| alloc_spec := primitive_alloc_spec;
      free_spec := primitive_free_spec;
      load_spec := primitive_load_spec;
diff --git a/iris_heap_lang/lib/clairvoyant_coin.v b/iris_heap_lang/lib/clairvoyant_coin.v
index eedba0d88..64fb01617 100644
--- a/iris_heap_lang/lib/clairvoyant_coin.v
+++ b/iris_heap_lang/lib/clairvoyant_coin.v
@@ -24,7 +24,7 @@ Definition toss_coin : val :=
   "c" <- "r";; resolve_proph: "p" to: "r";; #().
 
 Section proof.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition prophecy_to_list_bool (vs : list (val * val)) : list bool :=
     (λ v, bool_decide (v = #true)) ∘ snd <$> vs.
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index c4a4a0357..334e091df 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -20,7 +20,7 @@ Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
 Proof. solve_inG. Qed.
 
 Section mono_proof.
-  Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
+  Context `{!heapGS Σ, !mcounterG Σ} (N : namespace).
 
   Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
     ∃ n, own γ (● (MaxNat n)) ∗ l ↦ #n.
@@ -94,7 +94,7 @@ Global Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
 Proof. solve_inG. Qed.
 
 Section contrib_spec.
-  Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
+  Context `{!heapGS Σ, !ccounterG Σ} (N : namespace).
 
   Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
     ∃ n, own γ (●F n) ∗ l ↦ #n.
diff --git a/iris_heap_lang/lib/diverge.v b/iris_heap_lang/lib/diverge.v
index 18a27c2f2..cc6fb28eb 100644
--- a/iris_heap_lang/lib/diverge.v
+++ b/iris_heap_lang/lib/diverge.v
@@ -20,7 +20,7 @@ explicit error handling when the full capacity has already been reached. *)
 Definition diverge : val :=
   rec: "diverge" "v" := "diverge" "v".
 
-Lemma wp_diverge `{!heapG Σ} s E (Φ : val → iProp Σ) (v : val) :
+Lemma wp_diverge `{!heapGS Σ} s E (Φ : val → iProp Σ) (v : val) :
   ⊢ WP diverge v @ s;E {{ Φ }}.
 Proof.
   iLöb as "IH". wp_lam. iApply "IH".
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 4887a01cc..bf82e9b84 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -11,7 +11,7 @@ atomicity. *)
 (** First: logically atomic increment directly on top of the physical heap. *)
 
 Section increment_physical.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition incr_phy : val :=
     rec: "incr" "l" :=
@@ -38,7 +38,7 @@ End increment_physical.
 (** Next: logically atomic increment on top of an arbitrary logically atomic heap *)
 
 Section increment.
-  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
 
   Import atomic_heap.notation.
 
@@ -145,7 +145,7 @@ Section increment.
 End increment.
 
 Section increment_client.
-  Context `{!heapG Σ, !spawnG Σ}.
+  Context `{!heapGS Σ, !spawnG Σ}.
 
   Local Existing Instance primitive_atomic_heap.
 
diff --git a/iris_heap_lang/lib/lazy_coin.v b/iris_heap_lang/lib/lazy_coin.v
index cc7fdefdc..141b1955d 100644
--- a/iris_heap_lang/lib/lazy_coin.v
+++ b/iris_heap_lang/lib/lazy_coin.v
@@ -17,7 +17,7 @@ Definition read_coin : val :=
   end.
 
 Section proof.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition val_to_bool (v : val) : bool := bool_decide (v = #true).
 
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index bc7d88da8..a06b580b9 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import primitive_laws notation.
 From iris.prelude Require Import options.
 
-Structure lock Σ `{!heapG Σ} := Lock {
+Structure lock Σ `{!heapGS Σ} := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
@@ -38,5 +38,5 @@ Global Arguments locked {_ _} _ _.
 
 Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Global Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
+Global Instance is_lock_proper Σ `{!heapGS Σ} (L: lock Σ) γ lk:
   Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/nondet_bool.v b/iris_heap_lang/lib/nondet_bool.v
index f81d48cce..082c086d3 100644
--- a/iris_heap_lang/lib/nondet_bool.v
+++ b/iris_heap_lang/lib/nondet_bool.v
@@ -7,7 +7,7 @@ Definition nondet_bool : val :=
   λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
 
 Section proof.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma nondet_bool_spec : {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}.
   Proof.
diff --git a/iris_heap_lang/lib/par.v b/iris_heap_lang/lib/par.v
index ad4046100..8fb524dac 100644
--- a/iris_heap_lang/lib/par.v
+++ b/iris_heap_lang/lib/par.v
@@ -16,7 +16,7 @@ Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
-Context `{!heapG Σ, !spawnG Σ}.
+Context `{!heapGS Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been
    brought together.  That is strictly stronger than first stripping a later
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 66fe28f78..f2f9aa9c9 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -18,7 +18,7 @@ Definition join : val :=
     end.
 
 (** The CMRA & functor we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
@@ -27,7 +27,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!heapG Σ, !spawnG Σ} (N : namespace).
+Context `{!heapGS Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 050bc4fad..1a3ed783f 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -13,7 +13,7 @@ Definition acquire : val :=
 Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
@@ -21,7 +21,7 @@ Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapG Σ, !lockG Σ}.
+  Context `{!heapGS Σ, !lockG Σ}.
   Let N := nroot .@ "spin_lock".
 
   Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
@@ -102,7 +102,7 @@ End proof.
 
 Typeclasses Opaque is_lock locked.
 
-Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapGS Σ, !lockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index a36221a3a..a6b343d71 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -36,7 +36,7 @@ Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapG Σ, !tlockG Σ}.
+  Context `{!heapGS Σ, !tlockG Σ}.
   Let N := nroot .@ "ticket_lock".
 
   Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
@@ -172,7 +172,7 @@ End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapGS Σ, !tlockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 87adf2a6b..d4e9f2484 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -10,14 +10,14 @@ From iris.heap_lang Require Export class_instances.
 From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
 
-Class heapG Σ := HeapG {
-  heapG_invG : invG Σ;
-  heapG_gen_heapG :> gen_heapG loc (option val) Σ;
-  heapG_inv_heapG :> inv_heapG loc (option val) Σ;
-  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
+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) Σ;
 }.
 
-Global Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
+Global Instance heapG_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp σ _ κs _ :=
     (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
@@ -43,7 +43,7 @@ Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V)
 make setoid rewriting in the predicate [I] work we need actual definitions
 here. *)
 Section definitions.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Definition inv_mapsto_own (l : loc) (v : val) (I : val → Prop) : iProp Σ :=
     inv_mapsto_own l (Some v) (from_option I False).
   Definition inv_mapsto (l : loc) (I : val → Prop) : iProp Σ :=
@@ -60,7 +60,7 @@ Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
 Section lifting.
-Context `{!heapG Σ}.
+Context `{!heapGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val → iProp Σ.
 Implicit Types efs : list expr.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 528142133..2d78d4319 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -6,11 +6,11 @@ From iris.heap_lang Require Import notation.
 From iris.prelude Require Import options.
 Import uPred.
 
-Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
+Lemma tac_wp_expr_eval `{!heapGS Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
-Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
+Lemma tac_twp_expr_eval `{!heapGS Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
@@ -28,7 +28,7 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
   end.
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
-Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -40,7 +40,7 @@ Proof.
   pose proof @pure_exec_fill.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{!heapG Σ} Δ s E K e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapGS Σ} Δ s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
@@ -52,17 +52,17 @@ Proof.
   rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value_nofupd `{!heapG Σ} Δ s E Φ v :
+Lemma tac_wp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value_nofupd `{!heapG Σ} Δ s E Φ v :
+Lemma tac_twp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 
-Lemma tac_wp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
+Lemma tac_wp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. by rewrite wp_value_fupd. Qed.
-Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
+Lemma tac_twp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
 
@@ -170,12 +170,12 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
 Tactic Notation "wp_pair" := wp_pure (Pair _ _).
 Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
 
-Lemma tac_wp_bind `{!heapG Σ} K Δ s E Φ e f :
+Lemma tac_wp_bind `{!heapGS Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
-Lemma tac_twp_bind `{!heapG Σ} K Δ s E Φ e f :
+Lemma tac_twp_bind `{!heapGS Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
   envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
@@ -206,7 +206,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
 
 (** Heap tactics *)
 Section heap.
-Context `{!heapG Σ}.
+Context `{!heapGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/iris_heap_lang/total_adequacy.v b/iris_heap_lang/total_adequacy.v
index cdda3d067..327a287c1 100644
--- a/iris_heap_lang/total_adequacy.v
+++ b/iris_heap_lang/total_adequacy.v
@@ -4,8 +4,8 @@ From iris.heap_lang Require Export adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
-Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
-  (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
+Definition heap_total Σ `{!heapGpreS Σ} s e σ φ :
+  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
   sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
@@ -16,5 +16,5 @@ Proof.
   iExists
     (λ σ κs _, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
     (λ _, True%I); iFrame.
-  iApply (Hwp (HeapG _ _ _ _ _)). done.
+  iApply (Hwp (HeapGS _ _ _ _ _)). done.
 Qed.
diff --git a/tests/algebra.v b/tests/algebra.v
index fa9931e01..ec82c5740 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -12,7 +12,7 @@ Proof. reflexivity. Qed.
 Global Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
 
 Section tests.
-  Context `{!invG Σ}.
+  Context `{!invGS Σ}.
 
   Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
     λne P v, (▷ (P v))%I.
diff --git a/tests/atomic.v b/tests/atomic.v
index 00d34adde..a621a8ce7 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Unset Mangle Names.
 
 Section tests.
-  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
   Import atomic_heap.notation.
 
   (* FIXME: removing the `val` type annotation breaks printing. *)
@@ -20,7 +20,7 @@ End tests.
 
 (* Test if we get reasonable error messages with non-laterable assertions in the context. *)
 Section error.
-  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
   Import atomic_heap.notation.
 
   Check "non_laterable".
@@ -37,7 +37,7 @@ End error.
 (* Test if AWP and the AU obtained from AWP print. *)
 Check "printing".
 Section printing.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition code : expr := #().
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index cb7c84810..169e77d2f 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Unset Mangle Names.
 
 Section tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
 
@@ -329,7 +329,7 @@ Section tests.
 End tests.
 
 Section mapsto_tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   (* Test that the different versions of mapsto work with the tactics, parses,
      and prints correctly. *)
@@ -371,7 +371,7 @@ Section mapsto_tests.
 End mapsto_tests.
 
 Section inv_mapsto_tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
@@ -387,7 +387,7 @@ Section inv_mapsto_tests.
 End inv_mapsto_tests.
 
 Section atomic.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
 
   (* These tests check if a side-condition for [Atomic] is generated *)
@@ -417,7 +417,7 @@ Section atomic.
 End atomic.
 
 Section printing_tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma ref_print :
     True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
@@ -468,7 +468,7 @@ Section printing_tests.
 End printing_tests.
 
 Section error_tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Check "not_cmpxchg".
   Lemma not_cmpxchg :
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 85b25b90b..8d72a987c 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Unset Mangle Names.
 
 Section printing_tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma vs_print (P Q : iProp Σ) :
     P ={⊤}=∗ Q.
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 8b59a127d..4d8e5f234 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
 Section tests.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 9f2cc5842..24abfeda8 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -55,7 +55,7 @@ preconditions, in sort of `CPS` style, so that they can be applied easier when
 proving client code. A version of [list_reverse] in that style can be found in
 the file [theories/tests/list_reverse.v]. *)
 Section list_reverse.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Notation iProp := (iProp Σ).
   Implicit Types l : loc.
 
@@ -109,7 +109,7 @@ under max can be found in [theories/heap_lang/lib/counter.v]. *)
 update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
-Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
+Lemma wp_inv_open `{!irisGS Λ Σ} N E P e Φ :
   nclose N ⊆ E → Atomic WeaklyAtomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
@@ -190,7 +190,7 @@ Global Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section counter_proof.
-  Context `{!heapG Σ, !counterG Σ}.
+  Context `{!heapGS Σ, !counterG Σ}.
   Implicit Types l : loc.
 
   Definition I (γ : gname) (l : loc) : iProp Σ :=
diff --git a/tests/iris_notation.v b/tests/iris_notation.v
index 3e6fb5536..735ef8d0b 100644
--- a/tests/iris_notation.v
+++ b/tests/iris_notation.v
@@ -24,7 +24,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invG Σ}.
+  Context `{!invGS Σ}.
   Implicit Types P Q R : iProp Σ.
 
   (* Test scopes for bupd and fupd *)
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 3ecdbbe08..04d426610 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Unset Mangle Names.
 
 Section list_reverse.
-Context `{!heapG Σ}.
+Context `{!heapGS Σ}.
 Implicit Types l : loc.
 
 Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 0f93ccabf..90773c2b9 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -38,7 +38,7 @@ Proof. solve_inG. Qed.
 
 Section proof.
 Local Set Default Proof Using "Type*".
-Context `{!heapG Σ, !one_shotG Σ}.
+Context `{!heapGS Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
   (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
@@ -109,7 +109,7 @@ Definition client : expr :=
   (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
 
 Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+  Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
 
   Lemma client_safe : ⊢ WP client {{ _, True }}.
   Proof using Type*.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 4b858ca73..e929cfd14 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -35,7 +35,7 @@ Proof. solve_inG. Qed.
 
 Section proof.
 Local Set Default Proof Using "Type*".
-Context `{!heapG Σ, !one_shotG Σ}.
+Context `{!heapGS Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
   (l ↦ NONEV ∗ own γ (Pending (1/2)%Qp) ∨
@@ -127,7 +127,7 @@ Definition client : expr :=
   (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
 
 Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+  Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
 
   Lemma client_safe : ⊢ WP client {{ _, True }}.
   Proof using Type*.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index ebc45c6e5..fa04cc2a5 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -58,7 +58,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
+  Context `{!invGS Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
@@ -236,7 +236,7 @@ Section iris_tests.
 End iris_tests.
 
 Section monpred_tests.
-  Context `{!invG Σ}.
+  Context `{!invGS Σ}.
   Context {I : biIndex}.
   Local Notation monPred := (monPred I (iPropI Σ)).
   Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index f8601d2b0..955fb532c 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -52,7 +52,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
+  Context `{!invGS Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
@@ -242,7 +242,7 @@ Section iris_tests.
 End iris_tests.
 
 Section monpred_tests.
-  Context `{!invG Σ}.
+  Context `{!invGS Σ}.
   Context {I : biIndex}.
   Local Notation monPred := (monPred I (iPropI Σ)).
   Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 80612f2c0..990f81f2a 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -178,7 +178,7 @@ Section tests.
 End tests.
 
 Section tests_iprop.
-  Context {I : biIndex} `{!invG Σ}.
+  Context {I : biIndex} `{!invGS Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
   Implicit Types P Q R : monPred.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index b68e2e1a3..7f830cba2 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -8,7 +8,7 @@ Inductive tree :=
   | leaf : Z → tree
   | node : tree → tree → tree.
 
-Fixpoint is_tree `{!heapG Σ} (v : val) (t : tree) : iProp Σ :=
+Fixpoint is_tree `{!heapGS Σ} (v : val) (t : tree) : iProp Σ :=
   match t with
   | leaf n => ⌜v = InjLV #n⌝
   | node tl tr =>
@@ -34,7 +34,7 @@ Definition sum' : val := λ: "t",
   sum_loop "t" "l";;
   !"l".
 
-Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
+Lemma sum_loop_wp `{!heapGS Σ} v t l (n : Z) :
   [[{ l ↦ #n ∗ is_tree v t }]]
     sum_loop v #l
   [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
@@ -52,7 +52,7 @@ Proof.
     iExists ll, lr, vl, vr. by iFrame.
 Qed.
 
-Lemma sum_wp `{!heapG Σ} v t :
+Lemma sum_wp `{!heapGS Σ} v t :
   [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
 Proof.
   iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
-- 
GitLab