diff --git a/CHANGELOG.md b/CHANGELOG.md
index d798d12a578cffcac80a12e0d3c612bbea0882df..f93680cbf4ee084c54cc456c2e05423d59872f8a 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 e97efd204f4845d326dec3a38630b12caa29f71c..5e4e603488b713b3e55b9088b6e3144a914eecf8 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` type class with 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/docs/resource_algebras.md b/docs/resource_algebras.md
index fb59163a10bd29a801230415598b269c527ec168..3071a61facba722507a5bc6ec096c75add6f0619 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -7,7 +7,8 @@ that when dealing with higher-order ghost state -- see "Camera functors" below.)
 
 In our proofs, we always keep the `Î£` universally quantified to enable composition of proofs.
 Each proof just assumes that some particular resource algebras are contained in that global list.
-This is expressed via the `inG Î£ R` typeclass, which roughly says that `R âˆˆ Î£`.
+This is expressed via the `inG Î£ R` typeclass, which roughly says that `R âˆˆ Î£`
+("`R` is in the `G`lobal list of RAs `Î£` -- hence the `G`).
 
 Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
 not have to expose to clients what exactly their resource algebras are. For
@@ -112,46 +113,50 @@ Proof. apply (heap_adequacy clientÎ£)=> ?. apply client_safe. Qed.
 Some Iris modules involve a form of "global state".  For example, defining the
 `â†¦` for HeapLang involves a piece of ghost state that matches the current
 physical heap.  The `gname` of that ghost state must be picked once when the
-proof starts, and then globally known everywhere.  Hence `gen_heapG`, the type
+proof starts, and then globally known everywhere.  Hence `gen_heapGS`, the type
 class for the generalized heap module, bundles the usual `inG` assumptions
 together with the `gname`:
 ```coq
-Class gen_heapPreG (L V : Type) (Î£ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Î£ (authR (gen_heapUR L V))
+Class gen_heapGpreS (L V : Type) (Î£ : gFunctors) `{Countable L} := {
+  gen_heapGpreS_heap :> ghost_mapG Î£ L V;
 }.
-Class gen_heapG (L V : Type) (Î£ : gFunctors) `{Countable L} := {
-  gen_heap_inG :> gen_heapPreG L V Î£;
-  gen_heap_name : gname
+Class gen_heapGS (L V : Type) (Î£ : gFunctors) `{Countable L} := GenHeapGS {
+  gen_heap_inG :> gen_heapGpreS L V Î£;
+  gen_heap_name : gname;
 }.
 ```
+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
+might have different `gname`s, so `â†¦` based on these two distinct instances
+would be incompatible with each other.
 
-The `gen_heapPreG` typeclass (without the singleton data) is relevant for
-initialization, i.e., to create an instance of `gen_heapG`. This is happening as
+The `gen_heapGpreS` typeclass (without the singleton data) is relevant for
+initialization, i.e., to create an instance of `gen_heapGS`. This is happening as
 part of [`heap_adequacy`](iris_heap_lang/adequacy.v) using the
-initialization lemma for `gen_heapG` from
+initialization lemma for `gen_heapGS` from
 [`gen_heap_init`](iris/base_logic/lib/gen_heap.v):
 ```coq
-Lemma gen_heap_init `{gen_heapPreG L V Î£} Ïƒ :
-  (|==> âˆƒ _ : gen_heapG L V Î£, gen_heap_ctx Ïƒ)%I.
+Lemma gen_heap_init `{gen_heapGpreS L V Î£} Ïƒ :
+  (|==> âˆƒ _ : gen_heapGS L V Î£, gen_heap_ctx Ïƒ)%I.
 ```
 These lemmas themselves only make assumptions the way normal modules (those
-without global state) do. Just like in the normal case, `somethingPreG` type
+without global state) do. Just like in the normal case, `somethingGpreS` type
 classes have an `Instance` showing that a `subG` is enough to instantiate them:
 ```coq
-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.
 ```
-The initialization lemma then shows that the `somethingPreG` type class is
-enough to create an instance of the main `somethingG` class *below a view
+The initialization lemma then shows that the `somethingGpreS` type class is
+enough to create an instance of the main `somethingGS` class *below a view
 shift*.  This is written with an existential quantifier in the lemma because the
 statement after the view shift (`gen_heap_ctx Ïƒ` in this case) depends on having
-an instance of `gen_heapG` in the context.
+an instance of `gen_heapGS` in the context.
 
 Given that these global ghost state instances are singletons, they must be
-assumed explicitly everywhere.  Bundling `heapG` in a module type class like
-`one_shotG` would lose track of the fact that there exists just one `heapG`
-instance that is shared by everyone.
+assumed explicitly everywhere.  Bundling `heapGS` in a (non-singleton) module
+type class like `one_shotG` would lose track of the fact that there exists just
+one `heapGS` instance that is shared by everyone.
 
 ## Advanced topic: Camera functors and higher-order ghost state
 
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index ca565ab8c2816234aa73fcd164baa4dcf4f38151..68ac12c2427959895c039a6d577cad94c739aeb9 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 c74b89b6374534ba46edf717280333acea8c4545..88b0cda572e65a1bf4694c7d42b4ae1df7586638 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 c7d7a40503bc53986c448e1c2a71e6b4bbe37134..3feb1b40cdb439053541a794f7e7bf4e3b4364a0 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 005a01456d8c28c0cab063bbdb8c1a6b0eaa9464..a0a086c8deba6f71aa37f674d6450773ea30f86f 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 ecb038af207aada01a50cbb501931fac3d2a0fb6..2e196fbd9c11858c6bd9293707a727639477148b 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 91f87d5deda33c5e767ac397fd70e00696d6fe3b..620c5994e805de3324683e76cc1f4c670099b087 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 d4858462d05fe9f828fe7e1176ca2d0cac30e5ec..1f44bab6eb109064912b75930dc4be8975c36b5e 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 121e42e621c47e7b48f4368914bce8c78732471f..44d78abe6d76da090683c7082f71f996e213f36e 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 bbfc5a9e9b8d1b47204dcebba37ae9344ae29d7f..fd6546c97fb7c3520820d81d560751f6dd932c35 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 d9340a5ccd1f21cd0f4fc6bb27359603384c385c..2b06be13b600bc31191179c818239a1cefe43c87 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 fead228df60357bf52b3c5a31bedb5a3c02bd9cd..97ea858a7edf3d744994448f9120699d61d0ce75 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 468b0bfa6b6c5bf684ff6f91d1c1abda6a8fb594..1dd14d2b21d473d2b55a07c450fc4b5cf7939950 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 1a5aaca96a2652cb503d9b8e65a4cc6dfe685a18..edc7b8f81796023de05ef97b98b70181cafacef3 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 b160c1b62ee6662e4b888d574a314be56fd41746..60d7e4507d7fe474042b72e3feac3fd0375d2476 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 d1c470c586b6426bddd2d6b0bca0b561015f84c3..ed100b2d8a091dead7ae550a27674bbd35a6489e 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 35d776409cc259cc1617f48f157ef21c1868ee0e..473b61acb7fda9a255b61ca501977ed076c61cc1 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 101bf4d62f83e8fed0369015956ef499e1f99ee7..aac06d858ba1e4975343862e58535c177f755893 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 8b98e91aee33b04f062fd898da0f6e543565696b..7ef86fa5bf6b2884e98731fb1f79cf11d2bbab24 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 e3656a5dd934e7c3c4214d62465e1fb54467dfc5..bb54d99620522901afaf95a321b1396f3b35724c 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 64b121384150410f226f6460242e15faa0b26647..451cf54e1a46fb0d743a0052a98b1049ecd6cdd2 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 0f05f12325ace0f47172d214656d5e675bbce647..b8047cea765faffe88dbf6f4214cfd3edfd3799a 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 c2a571e9475161ee4796114a9dff904181a2d843..379bf4265e7a3cbd0e23a4372e40d29e2e9aa750 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 c40fa8df9cb6ad01771ee4fdbe5119856d680cfc..8ff987966f46fbc6dc97a71f79118a0a24e22eb6 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 d24fe5afd688caed7823936c38c27243e1faec04..3ce089faca66180d9fc8d2e19866c25f80785f74 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 0a812eef8ea772fee6620b6632b0a8ece85777c6..66a870aa54a5a58768076e1893e79d0c5b267c44 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 8a2165ce6becbac4b2e21575bfa4ef66d3abcd62..17f037256aa5eb72d41ecbd8b704821aa7915ea3 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 86598a764c749236289e61dc46eb0341aa83c35e..4508f0fefa0c9dd8d817ae45a82081eb44c1a0eb 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 160377bc09a0be2b48da050d87ae30aaad57c853..a63b674ec8284c46f398a953f01aeb3c32c96993 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 c095508e84f4ad7448895814cc6a2b16ab788c50..302215a8af72c74b5707bd6bbcbae67d0db62c2b 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 eedba0d8833a7485383f02a61cf3f95350f76de1..64fb016177497d0ac208238099ca9a49ae674cff 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 c4a4a0357adb56472bd36215ab8d4ce9963036ec..334e091df3270fcc4f83d515fb27d2a4c5615ce2 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 18a27c2f2cd7bf135804e6d313e901f24c00623e..cc6fb28ebb726c43b81cda573bf1a47657238da8 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 4887a01cc0b59aa2fa7c613672c7fb02d0e4cdb0..bf82e9b843e54dcc8dc1cfe15303424a5fd15f44 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 cc7fdefdc69621cfc4ba16b5401144c5a95d5030..141b1955dedcd00e9a940c2c5d9c682270eda0f8 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 bc7d88da8bb916c571b76c39af1e42665da13af1..a06b580b9714d50c61ac85b9d0f526328e8b656d 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 f81d48ccebbe3e877eb3fa33f4336586fd5556f2..082c086d31d8d6089834e5e081c8c38f30936c32 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 ad40461004a8d3050db35a43eddf937c261b8684..8fb524dac5ea11f54c32b97ea1ab4e1b92cd054a 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 66fe28f78ac7e3ba653c749b90f0bae34dd217c3..f2f9aa9c987cee0397a0745cd75dac8077284dec 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 050bc4fadde58c25de46ddbbbc41fd42324b7675..1a3ed783ff39eaacf63becad029bbfa9bfbfc0f1 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 a36221a3a58b05d003fa2e563871a48d0bb73256..a6b343d7145d2f5370483d415f4238a29b2d1f6a 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 87adf2a6b1a1d6aa7c4207e46c95fce3d18b4b59..d4e9f24847b5dde0f7edf86e675e4fd7898c6195 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 5281421337e57053fbb0411bfddc994c20778003..2d78d4319c941f329510af9964d614001fd25e5a 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 cdda3d0677c776720b2ee81bc996d793460b1df7..327a287c1c9329e06c6266264fb60f79f281bd17 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 fa9931e016f1bfc2c9281227cb7036f016beff4e..ec82c57404bbb73cec3b2b50b39688da4dfe0ad2 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.ref b/tests/atomic.ref
index 859bb6deb7e32902cf459b362c807d7e09ea45b6..8bf105a88b974cce1d8b3ddbf9551365d7851f48 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   aheap : atomic_heap Î£
   Q : iProp Î£
   l : loc
@@ -23,14 +23,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   P : val â†’ iProp Î£
   ============================
   âŠ¢ <<< âˆ€ x : val, P x >>> code @ âŠ¤ <<< âˆƒ y : val, P y, RET #() >>>
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   P : val â†’ iProp Î£
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -41,7 +41,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   P : val â†’ iProp Î£
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -55,14 +55,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< âˆ€ x : val, l â†¦ x >>> code @ âŠ¤ <<< l â†¦ x, RET #() >>>
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -73,7 +73,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -86,14 +86,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< l â†¦ #() >>> code @ âŠ¤ <<< âˆƒ y : val, l â†¦ y, RET #() >>>
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -104,7 +104,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -118,14 +118,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< l â†¦ #() >>> code @ âŠ¤ <<< l â†¦ #(), RET #() >>>
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -136,7 +136,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -151,7 +151,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< âˆ€ x : val, l â†¦ x âˆ— l â†¦ x >>>
@@ -160,7 +160,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -172,7 +172,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< âˆ€ x : val, l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x >>>
@@ -181,7 +181,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -193,7 +193,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< âˆ€ xx : val, l â†¦ xx âˆ— l â†¦ xx âˆ— l â†¦ xx >>>
@@ -203,7 +203,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -217,7 +217,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   âŠ¢ <<< âˆ€ x : val, l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x âˆ— l â†¦ x >>>
@@ -226,7 +226,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
@@ -238,7 +238,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   x : val
   ============================
@@ -248,7 +248,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   x : val
   Î¦ : language.val heap_lang â†’ iProp Î£
@@ -261,7 +261,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   x : val
   ============================
@@ -271,7 +271,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   x : val
   Î¦ : language.val heap_lang â†’ iProp Î£
@@ -284,7 +284,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   xx, yyyy : val
   ============================
@@ -294,7 +294,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   xx, yyyy : val
   Î¦ : language.val heap_lang â†’ iProp Î£
@@ -307,7 +307,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   xx, yyyy : val
   ============================
@@ -318,7 +318,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   xx, yyyy : val
   Î¦ : language.val heap_lang â†’ iProp Î£
@@ -334,7 +334,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   P : val â†’ iProp Î£
   Î¦ : language.val heap_lang â†’ iProp Î£
   ============================
diff --git a/tests/atomic.v b/tests/atomic.v
index 00d34addeb86e0212741ea1a427cd6e9e23134b6..a621a8ce7715c5dbc7184e93d71f04cf7a5e1ade 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.ref b/tests/heap_lang.ref
index 64e37382064e716331fc28ad29f4b1d9f4bea613..e5af6aef4d1abfa468a63f4a5dd6a2630fcba346 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -3,7 +3,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   E : coPset
   ============================
   --------------------------------------âˆ—
@@ -12,7 +12,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   E : coPset
   l : loc
   ============================
@@ -25,7 +25,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   E : coPset
   l : loc
   ============================
@@ -37,7 +37,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   E : coPset
   l, l' : loc
   ============================
@@ -51,7 +51,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   _ : â–· l â†¦ #0
@@ -61,7 +61,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   _ : l â†¦ #1
@@ -97,7 +97,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   "Hl1" : l â†¦{#1 / 2} #0
@@ -108,7 +108,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   ============================
   --------------------------------------âˆ—
@@ -122,7 +122,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   ============================
   --------------------------------------âˆ—
   WP "x" {{ _, True }}
@@ -130,7 +130,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   n : Z
   H : (0 < n)%Z
   Î¦ : val â†’ iPropI Î£
@@ -146,7 +146,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   vs : list val
   ============================
@@ -160,7 +160,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   v : val
   ============================
   --------------------------------------âˆ—
@@ -171,7 +171,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   v : val
   ============================
   --------------------------------------âˆ—
@@ -180,7 +180,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   v : val
   Î¦ : val â†’ iPropI Î£
@@ -194,7 +194,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   dq : dfrac
   l : loc
   v : val
@@ -208,7 +208,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   l : loc
   I : val â†’ Prop
   Heq : âˆ€ v : val, I v â†” I #true
@@ -219,7 +219,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 2 goals
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   E1, E2 : coPset
   P : iProp Î£
   ============================
@@ -235,7 +235,7 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 2 goals
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   N : namespace
   E : coPset
   P : iProp Î£
@@ -254,7 +254,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N,E}=> True }}
 2 goals
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   N : namespace
   E : coPset
   P : iProp Î£
@@ -270,7 +270,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N}=> â–· P âˆ— True }}
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   ============================
   --------------------------------------âˆ—
   WP let: "f" := Î»: "x", "x" in ref ("f" #10) {{ _, True }}
@@ -278,7 +278,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N}=> â–· P âˆ— True }}
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------âˆ—
@@ -290,7 +290,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N}=> â–· P âˆ— True }}
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   Î¦ : language.val heap_lang â†’ iPropI Î£
   ============================
@@ -303,7 +303,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N}=> â–· P âˆ— True }}
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   Î¦ : language.val heap_lang â†’ iPropI Î£
   E : coPset
@@ -317,7 +317,7 @@ WP #() #() @ E âˆ– â†‘N {{ _, |={E âˆ– â†‘N}=> â–· P âˆ— True }}
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index cb7c84810285a63b361ba9d7ef6d8639528a8cb1..169e77d2f6fca8a7d27e17f49869893612ea3f40 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.ref b/tests/heap_lang2.ref
index dff62fa87c541d8a9c6fd3ef8e0197c946d5bf88..1c677e63f410219d4b8a5dc654cfb13f0e4dfd42 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,14 +1,14 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   P, Q : iProp Î£
   ============================
   P ={âŠ¤}=âˆ— Q
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------âˆ—
@@ -20,7 +20,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 85b25b90be4b4f34f65ee5b0b525303b68ab4224..8d72a987c7b91b5ba485b930ccc27cd159d6efa8 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 8b59a127df2d145161968b84dd01dd9eb7439511..4d8e5f234aca1beb04ff1d355b0ad53120c6d11c 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.ref b/tests/ipm_paper.ref
index 74a366e9c6f993d80297e8e81cce620007254729..d7ba9448abfccedb64306a3210c46f8a8568b2ab 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -66,7 +66,7 @@ P
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   counterG0 : counterG Î£
   l : loc
   n : nat
@@ -82,7 +82,7 @@ P
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   counterG0 : counterG Î£
   l : loc
   n : nat
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 9f2cc58424df35971260f7be5bb23812fa11cc9a..24abfeda8ba64783e25a2dc74f200f6e928a0129 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 3e6fb553694c636e6256ff94da9f05e231c5e512..735ef8d0b4da5e72e17fe647b081abb84875a6c1 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.ref b/tests/list_reverse.ref
index b92601d2c985bc7b8030798397c05f7b8be60bac..cd47ff4bdd1763eb219c002b3b74f50dd5d0308e 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   hd, acc : val
   xs, ys : list val
   Î¦ : val â†’ iPropI Î£
@@ -15,7 +15,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   acc : val
   ys : list val
   Î¦ : val â†’ iPropI Î£
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 3ecdbbe082757f3447672285950b2ce11a38326d..04d426610523bf78984a3bcde83827f6a6f09759 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.ref b/tests/one_shot.ref
index 182ac473defb6f95ccc9eee57e01c738df35bc55..94a3ddc05772f1ed1db1cd01a26a0c45d7698dfc 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   one_shotG0 : one_shotG Î£
   Î¦ : val â†’ iProp Î£
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   one_shotG0 : one_shotG Î£
   Î¦ : val â†’ iProp Î£
   N : namespace
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 0f93ccabf3c022299caf3b963a2652fbe83d6ec5..90773c2b9821b4ea30d3f325bf78f0fc44d0c397 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.ref b/tests/one_shot_once.ref
index 686937f1065150df00ae611d3f68801822a9a8bf..4be43be0dc1b52d1098fb69503a0791d46ee5469 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   one_shotG0 : one_shotG Î£
   Î¦ : val â†’ iProp Î£
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Î£ : gFunctors
-  heapG0 : heapG Î£
+  heapGS0 : heapGS Î£
   one_shotG0 : one_shotG Î£
   Î¦ : val â†’ iProp Î£
   N : namespace
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 4b858ca73b34bc6627e4d73cb3c630510a4fbaa7..e929cfd145da951eafd28f98c62e66158e3458c7 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.ref b/tests/proofmode_ascii.ref
index 6c4fc6ad6fd4fb1001b0273627b8c254c91355cc..b0d84bf2c75c5d4b125f57031d216c7197c7210e 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   Î³ : gname
@@ -49,7 +49,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   Î³ : gname
@@ -68,7 +68,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   t : na_inv_pool_name
@@ -89,7 +89,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   t : na_inv_pool_name
@@ -120,7 +120,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   I : biIndex
   N : namespace
   E : coPset
@@ -136,7 +136,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index ebc45c6e531002e58e6b8f62ba3e075652dd8c36..fa04cc2a565bef12c094e298bef37cf7df39dea4 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.ref b/tests/proofmode_iris.ref
index dc20ed5696e88438d41e445c85d2448de207cd53..d049912e274832e8df70839ebb36fa384e240c9a 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,7 +1,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   Î³ : gname
@@ -43,7 +43,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   Î³ : gname
@@ -61,7 +61,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   Î³ : gname
@@ -80,7 +80,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   t : na_inv_pool_name
@@ -101,7 +101,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   t : na_inv_pool_name
@@ -115,7 +115,7 @@
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   t : na_inv_pool_name
@@ -146,7 +146,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   inG0 : inG Î£ fracR
@@ -160,7 +160,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   cinvG0 : cinvG Î£
   na_invG0 : na_invG Î£
   inG0 : inG Î£ fracR
@@ -175,7 +175,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   I : biIndex
   N : namespace
   E : coPset
@@ -191,7 +191,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   I : biIndex
   N : namespace
   E : coPset
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index f8601d2b09d2f69ae60165d367c487a5f6edea12..955fb532c1aa07f7f6579c30686cd0b9cc9a1cb7 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.ref b/tests/proofmode_monpred.ref
index be3c1169d610c66856153aa4fc6a107a03c0e9ac..4d1d96175d23bf8ca564feaab67ade0c4dde7c9a 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -63,7 +63,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   N : namespace
   ð“Ÿ : iProp Î£
   ============================
@@ -76,7 +76,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Î£ : gFunctors
-  invG0 : invG Î£
+  invGS0 : invGS Î£
   N : namespace
   ð“Ÿ : iProp Î£
   ============================
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 80612f2c065fdb6d776ebda867969ddd738039a4..990f81f2a64469f1e88aed418dfb565fe3edc7ba 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 b68e2e1a3828fbb98510ceafb16ffdd227345009..7f830cba20792efd502a46652a9cb74848ece660 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' /=.