diff --git a/opam b/opam
index fc9bcb0a5151c168026283e7cee2e6244786c9f8..bb48e99e70b03ed63c09fa71c88911450a57974d 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-05-27.2.59e3a162") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-06-03.0.2959900d") | (= "dev") }
 ]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 99e90d5d06734834c4c32b829978aa622ea24322..9e1380aeb9a2e628b92cf713ad65a8ace161e84b 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -92,7 +92,7 @@ Qed.
 Notation iProto Σ := (iProto Σ val).
 Notation iMsg Σ := (iMsg Σ val).
 
-Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
+Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
   ∃ γ s (l r : loc) (lk : val),
     ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
@@ -110,7 +110,7 @@ Instance: Params (@iProto_mapsto) 4 := {}.
 Notation "c ↣ p" := (iProto_mapsto c p)
   (at level 20, format "c  ↣  p").
 
-Instance iProto_mapsto_contractive `{!heapG Σ, !chanG Σ} c :
+Instance iProto_mapsto_contractive `{!heapGS Σ, !chanG Σ} c :
   Contractive (iProto_mapsto c).
 Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
 
@@ -130,7 +130,7 @@ Infix "<+>" := (iProto_choice Send True True) (at level 85) : proto_scope.
 Infix "<&>" := (iProto_choice Recv True True) (at level 85) : proto_scope.
 
 Section channel.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index a7091998e5d9e15076502fcf1e16afbcb665d3c7..8f4294bd0b203d18277b441e7a4868e9aa76de37 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -49,7 +49,7 @@ Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
 Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
 
 Section classes.
-  Context `{!chanG Σ, !heapG Σ}.
+  Context `{!chanG Σ, !heapGS Σ}.
   Implicit Types TT : tele.
   Implicit Types p : iProto Σ.
   Implicit Types m : iMsg Σ.
@@ -184,7 +184,7 @@ End classes.
 
 (** * Symbolic execution tactics *)
 (* TODO: Maybe strip laters from other hypotheses in the future? *)
-Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
+Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (<?> m) →
   MsgTele m tv tP tp →
@@ -273,7 +273,7 @@ Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_i
     simple_intropattern(x8) ")" constr(pat) :=
   wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
-Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
+Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (<!> m) →
   MsgTele m tv tP tp →
@@ -373,7 +373,7 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
   wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
                 eexists x6; eexists x7; eexists x8) with pat.
 
-Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
+Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
     c p P1 P2 (p1 p2 : iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
@@ -422,7 +422,7 @@ Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_in
   wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2). 
 Tactic Notation "wp_branch" := wp_branch as %_ | %_.
 
-Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
+Lemma tac_wp_select `{!chanG Σ, !heapGS Σ} Δ neg i js K
     c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 62a1972ddfd18a522b6f4e22f2671e531d7b9884..29b7e326a4a69506402d2be370cb3c39196dcad4 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -122,7 +122,7 @@ Definition prog_ref_swap_loop : val := λ: <>,
   !"l1" + !"l2".
 
 Section proofs.
-Context `{heapG Σ, chanG Σ}.
+Context `{heapGS Σ, chanG Σ}.
 
 (** Protocols for the respective programs *)
 Definition prot : iProto Σ :=
diff --git a/theories/examples/equivalence.v b/theories/examples/equivalence.v
index 73d5c3515c9e8817103ef93bda0c8cf3535f90c7..9bb81a5415d7e52875e87c015c5c0e135ab91823 100644
--- a/theories/examples/equivalence.v
+++ b/theories/examples/equivalence.v
@@ -1,7 +1,7 @@
 From actris.channel Require Import channel proofmode.
 
 Section equivalence_examples.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Lemma binder_swap_equivalence_example :
     ((<! (x y : Z)> MSG (#x,#y) ; END):iProto Σ)%proto ≡
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index a851ea08b64a17ab7c3fde4288620dc0c3fc96f2..0f65fc9189743024fb26c53628258940ce0373bf 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -13,7 +13,7 @@ Definition list_rev_client : val :=
     send "c" "l";; recv "c".
 
 Section list_rev_example.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Definition list_rev_prot : iProto Σ :=
     (<! (l : loc) (vs : list val)> MSG #l {{ llist internal_eq l vs }} ;
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 3f7832dc230b7c0977d3039080910313039e1031..9c3ae3357fbe03475de5b16b58cc6421b68bf1ba 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -96,7 +96,7 @@ Class map_reduceG Σ A B `{Countable A, Countable B} := {
 
 Section mapper.
   Context `{Countable A, Countable B} {C : Type}.
-  Context `{!heapG Σ, !chanG Σ, !map_reduceG Σ A B}.
+  Context `{!heapGS Σ, !chanG Σ, !map_reduceG Σ A B}.
   Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
   Context (map : A → list (Z * B)) (red : Z → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index 661369f545858ae4e36a3557499f65d579fd3f82..a4cd7c779d59ffd245ba2629a358ae7cecde9dfc 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -60,7 +60,7 @@ Class mapG Σ A `{Countable A} := {
 
 Section map.
   Context `{Countable A} {B : Type}.
-  Context `{!heapG Σ, !chanG Σ, !mapG Σ A}.
+  Context `{!heapGS Σ, !chanG Σ, !mapG Σ A}.
   Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
   Local Open Scope nat_scope.
   Implicit Types n : nat.
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index 75d9d7ffc538b35da7e100f78807b2489e799432..6180e2296754a2ea7637ef089a8da6a84a31a010 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -8,7 +8,7 @@ Inductive pizza :=
   | Calzone.
 
 Section example.
-  Context `{heapG Σ, chanG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
 
   Definition pizza_to_val (p : pizza) :=
     match p with
diff --git a/theories/examples/rpc.v b/theories/examples/rpc.v
index eefed48666cbdf340e7a828142a07b5373cd7c21..45332c62e067bd8bf01a51d48637a57ca93f660a 100644
--- a/theories/examples/rpc.v
+++ b/theories/examples/rpc.v
@@ -33,7 +33,7 @@ Definition program : val :=
     client (Fst "c").
 
 Section rpc_example.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
   Definition f_spec {T U} (IT : T → val → iProp Σ) (IU : U → val → iProp Σ)
              (f : T → U) (fv : val) : iProp Σ :=
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index e5df3a026abdad8808fa98ffcc372a3c34b6f3ea..03f95108f3a2cdff1296b58b201128f59f995a06 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -42,7 +42,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
   recv "c".
 
 Section sort.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
   Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
     (<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index c628d3ea08eaea58066e47759b5499032d584b4c..10ec01fa2667eaf8bf348033a7d99ef173c1a52c 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -34,7 +34,7 @@ Definition sort_service_br_del : val :=
     else #().
 
 Section sort_service_br_del.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
   Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
 
   Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 599c12d0f59e8132bfc57c9afd57772bd23526c3..f657fad94d659d4ccc7b7de13d375ac30872575e 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -72,7 +72,7 @@ Definition sort_client_fg : val := λ: "cmp" "xs",
   recv_all "c" "xs".
 
 Section sort_fg.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
   Section sort_fg_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 57030fd0cdd5cf248a0d71a9d899adb83c651b9d..c6842d47ba3a066d46e4bfaf4f7defa9b8fa0120 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -2,7 +2,7 @@ From actris.channel Require Import proofmode proto channel.
 From iris.proofmode Require Import tactics.
 
 Section subprotocol_basics.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Lemma reference_example (l1' : loc) :
     l1' ↦ #20 -∗
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 22adfcd013995d8ef72377c83b0e540ab1aa90c6..42446ee7e014a2ea956077083db87a0dc353b406 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -30,7 +30,7 @@ Definition swap_mapper_client : val :=
     send_all "c" "xs";; recv_all "c" "xs" "n";; send "c" #false.
 
 Section with_Σ.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
   Context {T U : Type}.
   Context (IT : T → val → iProp Σ).
   Context (IU : U → val → iProp Σ).
diff --git a/theories/logrel/examples/choice_subtyping.v b/theories/logrel/examples/choice_subtyping.v
index 68d3fbe390e20305a0fa0b3dc5910ce83ff9c210..09e72f7ffc84d08515fd017ac4d74da8d6a373f8 100644
--- a/theories/logrel/examples/choice_subtyping.v
+++ b/theories/logrel/examples/choice_subtyping.v
@@ -8,7 +8,7 @@ From actris.channel Require Import proofmode.
 From actris.logrel Require Import subtyping_rules.
 
 Section choice_example.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Variables Sr Sm Sp Sq Ss Su : ltty Σ.
   Variables Srm Ssm Srp Ssp Sr' : ltty Σ.
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 4e675a80b71c2ec208408ad2a29b4eac8c22fb74..97679f3e3cccadff1c17989d4ed03b5c862e3dd4 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -56,7 +56,7 @@ Definition compute_client : val :=
     recv_all_par "c" "ys" "n" "lk" "counter");; "ys".
 
 Section compute_example.
-  Context `{heapG Σ, chanG Σ, lockG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, lockG Σ, spawnG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition compute_type_client_aux (rec : lsty Σ) : lsty Σ :=
diff --git a/theories/logrel/examples/compute_service.v b/theories/logrel/examples/compute_service.v
index 1495297d181510da08ee99721930b156293e925b..38ec1655ae568392507d55cb89efa4773ebfa417 100644
--- a/theories/logrel/examples/compute_service.v
+++ b/theories/logrel/examples/compute_service.v
@@ -22,7 +22,7 @@ Definition compute_service : val :=
     (λ: "c", #()).
 
 Section compute_example.
-  Context `{heapG Σ, chanG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
 
   Definition compute_type_service_aux (rec : lsty Σ) : lsty Σ :=
     lty_branch $ <[cont := (<?? A> TY () ⊸ A; <!!> TY A ; rec)%lty]> $
diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index 55290e0badc3caf94748e28b289d86d61df35f93..0f46546b958f925459f64d2edbdcded67703b7f3 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -11,7 +11,7 @@ From actris.logrel Require Import term_typing_rules session_typing_rules.
 From actris.channel Require Import proofmode.
 
 Section mapper_example.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   (** Client type as dual of service type *)
   Definition mapper_client_type_aux (rec : lsty Σ) : lsty Σ :=
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index 7c57be0a628024f3be1b832230a1fa5d190d3a8f..cd7c10930dce30937bab0449a6e24faf5e341d56 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -62,7 +62,7 @@ Definition mapper_prog : val :=
    par_start (mapper_service) (mapper_client "f" "xs").
 
 Section mapper_example.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Definition mapper_type_rec_service_aux (A B : ltty Σ) (rec : lsty Σ) : lsty Σ :=
     lty_branch $ <[cont := (<??> TY A; <!!> TY B ; rec)%lty]>
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 34228f13226997481fa6478012ac9de8ecf11890..6f7a6a562f3448ee488ff0209a98e8e800c1480f 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -12,7 +12,7 @@ From iris.proofmode Require Import tactics.
 
 Definition prog : expr := λ: "c", (recv "c", recv "c").
 
-Lemma prog_typed `{heapG Σ, chanG Σ} :
+Lemma prog_typed `{heapGS Σ, chanG Σ} :
   [] ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
 Proof.
   iApply (ltyped_lam []); simpl. iApply ltyped_post_nil.
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 3f8e65424636a2f9b7c5cf96134f3995b4a5bf84..81e56a406924623684381a326fe5dbd88cae09af 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -33,7 +33,7 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{heapG Σ, chanG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition prog_prot : iProto Σ :=
@@ -117,7 +117,7 @@ Section double.
 End double.
 
 Section double_fc.
-  Context `{heapG Σ, chanG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
   Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
   Definition prog_prot_fc (P : val → val → iProp Σ) : iProto Σ :=
diff --git a/theories/logrel/examples/rec_subtyping.v b/theories/logrel/examples/rec_subtyping.v
index e1abf8a7ab968adef3dec1bcee09c0390a51e820..f536f57356a95e21b3a4ad0543f29173a3615b0d 100644
--- a/theories/logrel/examples/rec_subtyping.v
+++ b/theories/logrel/examples/rec_subtyping.v
@@ -9,7 +9,7 @@ From actris.channel Require Import proofmode.
 From actris.logrel Require Import subtyping_rules.
 
 Section basics.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
 
   Definition prot1_aux (rec : lsty Σ) : lsty Σ :=
     <!! X Y> TY (X ⊸ Y); <!!> TY X; <??> TY Y; rec.
diff --git a/theories/logrel/lib/list.v b/theories/logrel/lib/list.v
index 4ee66b8fba95b06a2df9451e552afdab68dfcaf8..3f5e64648139ec35bd4e9c86ddd2d6deb5c9b308 100644
--- a/theories/logrel/lib/list.v
+++ b/theories/logrel/lib/list.v
@@ -2,17 +2,17 @@ From actris.utils Require Import llist.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Import term_types.
 
-Definition lty_list_aux `{!heapG Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
+Definition lty_list_aux `{!heapGS Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
   ref_uniq (() + (A * X)).
-Instance lty_list_aux_contractive `{!heapG Σ} A :
+Instance lty_list_aux_contractive `{!heapGS Σ} A :
   Contractive (@lty_list_aux Σ _ A).
 Proof. solve_proto_contractive. Qed.
-Definition lty_list `{!heapG Σ} (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
+Definition lty_list `{!heapGS Σ} (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
 
 Notation "'list' A" := (lty_list A) (at level 10) : lty_scope.
 
 Section with_Σ.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma list_type_loc A v :
     ltty_car (list A) v -∗ ∃ (l : loc) , ⌜v = #l⌝.
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 47b1065e5c3870dce7b0693dac1d0c16d1e67720..9e2d5156fc02cb030b308b9b4e242c0d61bdac34 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -36,12 +36,12 @@ Definition mutex_release : val :=
   λ: "guard" "inner", Snd "guard" <- "inner";; release (Fst "guard").
 
 (** Semantic types *)
-Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+Definition lty_mutex `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (γ : gname) (l : loc) (lk : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I.
 
-Definition lty_mutex_guard `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+Definition lty_mutex_guard `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (γ : gname) (l : loc) (lk : val) (v : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
@@ -54,7 +54,7 @@ Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
 Notation "'mutex_guard' A" := (lty_mutex_guard A) (at level 10) : lty_scope.
 
 Section properties.
-  Context `{heapG Σ, lockG Σ}.
+  Context `{heapGS Σ, lockG Σ}.
   Implicit Types A : ltty Σ.
 
   Global Instance lty_mutex_contractive : Contractive lty_mutex.
@@ -98,7 +98,7 @@ Section properties.
 End properties.
 
 Section rules.
-  Context `{heapG Σ, lockG Σ}.
+  Context `{heapGS Σ, lockG Σ}.
 
   (** Mutex properties *)
   Lemma ltyped_mutex_alloc Γ A :
diff --git a/theories/logrel/lib/par_start.v b/theories/logrel/lib/par_start.v
index 5f0e2e2107d606e301d1459c21df5481c9a0e713..bdb11275a41d64ff65f6aaa65be90053d964573a 100644
--- a/theories/logrel/lib/par_start.v
+++ b/theories/logrel/lib/par_start.v
@@ -9,7 +9,7 @@ Definition par_start : expr := λ: "e1" "e2",
   let: "c2" := Snd "c" in
   ("e1" "c1") ||| ("e2" "c2").
 
-Lemma ltyped_par_start `{!heapG Σ, !chanG Σ, !spawnG Σ} Γ S A B :
+Lemma ltyped_par_start `{!heapGS Σ, !chanG Σ, !spawnG Σ} Γ S A B :
   Γ ⊨ par_start : (chan S ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ A * B.
 Proof.
   iApply (ltyped_lam []); iApply (ltyped_lam [CtxItem "e1" _] [] "e2"); simpl.
diff --git a/theories/logrel/napp.v b/theories/logrel/napp.v
index ecbda6896f575731755dd8bc5716ddbf177481e8..bccdac67d96cbbbe7cc530e04b55fb84fc3aa6b9 100644
--- a/theories/logrel/napp.v
+++ b/theories/logrel/napp.v
@@ -6,7 +6,7 @@ From actris.logrel Require Import term_typing_rules session_types subtyping_rule
 From actris.channel Require Import proofmode.
 
 Section with_Σ.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Fixpoint lty_napp (R : lsty Σ) (n : nat) :=
     match n with
diff --git a/theories/logrel/operators.v b/theories/logrel/operators.v
index 7abfb4ffdff154a8a302a0a33bc646396df7b7d5..267f47ec4e730b988ed80cf89580b187548fd4b7 100644
--- a/theories/logrel/operators.v
+++ b/theories/logrel/operators.v
@@ -29,9 +29,9 @@ Section operators.
   Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
   Global Instance lty_int_unboxed : LTyUnboxed (Σ:=Σ) lty_int.
   Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
-  Global Instance lty_ref_uniq_unboxed `{heapG Σ} A : LTyUnboxed (ref_uniq A).
+  Global Instance lty_ref_uniq_unboxed `{heapGS Σ} A : LTyUnboxed (ref_uniq A).
   Proof. iIntros (v). by iDestruct 1 as (i w ->) "?". Qed.
-  Global Instance lty_ref_shr_unboxed `{heapG Σ} A : LTyUnboxed (ref_shr A).
+  Global Instance lty_ref_shr_unboxed `{heapGS Σ} A : LTyUnboxed (ref_shr A).
   Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
 
   (** Rules for operator typing *)
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 1a2b24d4c37120026e58e1697761af497e3c154f..25b5c3a2025cffe5e842d7e671cbefa4347836f3 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -11,7 +11,7 @@ From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
 
 Section session_typing_rules.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
   Implicit Types A B : ltty Σ.
   Implicit Types S T : lsty Σ.
   Implicit Types Γ : ctx Σ.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index d87b685decafe52ac817bcfe70bd8c22aaad9720..321edfd013bf869dcebf9c31d5a82b8ed0ef467a 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 From actris.logrel Require Export subtyping term_types session_types.
 
 Section subtyping_rules.
-  Context `{heapG Σ, chanG Σ}.
+  Context `{heapGS Σ, chanG Σ}.
   Implicit Types A : ltty Σ.
   Implicit Types S : lsty Σ.
 
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 99dd8826761b03c46a92782d2fb9707c30a1dcbf..615562cdf0131a4d27db2742138d21909deaf43e 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -43,7 +43,7 @@ Definition lty_bool {Σ} : ltty Σ := Ltty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%
 Definition lty_int {Σ} : ltty Σ := Ltty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
 Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
 
-Definition lty_arr `{heapG Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
+Definition lty_arr `{heapGS Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
   ∀ v, ▷ ltty_car A1 v -∗ WP w v {{ ltty_car A2 }})%I.
 (* TODO: Make a non-linear version of prod, using ∧ *)
 Definition lty_prod {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
@@ -52,7 +52,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
   (∃ w1, ⌜w = InjLV w1⌝ ∗ ▷ ltty_car A1 w1) ∨
   (∃ w2, ⌜w = InjRV w2⌝ ∗ ▷ ltty_car A2 w2))%I.
 
-Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
+Definition lty_forall `{heapGS Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ X, WP w #() {{ ltty_car (C X) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ X, ▷ ltty_car (C X) w)%I.
@@ -60,13 +60,13 @@ Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
 Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
 Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
 
-Definition lty_ref_uniq `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+Definition lty_ref_uniq `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
 Definition ref_shrN := nroot .@ "shr_ref".
-Definition lty_ref_shr `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+Definition lty_ref_shr `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ □ ltty_car A v))%I.
 
-Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
+Definition lty_chan `{heapGS Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
   Ltty (λ w, w ↣ lsty_car P)%I.
 
 Instance: Params (@lty_copy) 1 := {}.
@@ -110,14 +110,14 @@ Section term_types.
   Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
   Proof. solve_proper. Qed.
 
-  Global Instance lty_arr_contractive `{heapG Σ} n :
+  Global Instance lty_arr_contractive `{heapGS Σ} n :
     Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
   Proof.
     intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
     f_equiv; [by f_contractive|].
     apply (wp_contractive _ _ _ _ _)=> v'. destruct n=> //=; by f_equiv.
   Qed.
-  Global Instance lty_arr_ne `{heapG Σ} : NonExpansive2 lty_arr.
+  Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
   Proof. solve_proper. Qed.
   Global Instance lty_prod_contractive n:
     Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
@@ -130,14 +130,14 @@ Section term_types.
   Global Instance lty_sum_ne : NonExpansive2 (@lty_sum Σ).
   Proof. solve_proper. Qed.
 
-  Global Instance lty_forall_contractive `{heapG Σ} k n :
+  Global Instance lty_forall_contractive `{heapGS Σ} k n :
     Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
   Proof.
     intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
     apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
     by destruct n as [|n]; simpl.
   Qed.
-  Global Instance lty_forall_ne `{heapG Σ} k n :
+  Global Instance lty_forall_ne `{heapGS Σ} k n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
   Proof. solve_proper. Qed.
   Global Instance lty_exist_contractive k n :
@@ -147,18 +147,18 @@ Section term_types.
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
   Proof. solve_proper. Qed.
 
-  Global Instance lty_ref_uniq_contractive `{heapG Σ} : Contractive lty_ref_uniq.
+  Global Instance lty_ref_uniq_contractive `{heapGS Σ} : Contractive lty_ref_uniq.
   Proof. solve_contractive. Qed.
-  Global Instance lty_ref_uniq_ne `{heapG Σ} : NonExpansive lty_ref_uniq.
+  Global Instance lty_ref_uniq_ne `{heapGS Σ} : NonExpansive lty_ref_uniq.
   Proof. solve_proper. Qed.
 
-  Global Instance lty_ref_shr_contractive `{heapG Σ} : Contractive lty_ref_shr.
+  Global Instance lty_ref_shr_contractive `{heapGS Σ} : Contractive lty_ref_shr.
   Proof. solve_contractive. Qed.
-  Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr.
+  Global Instance lty_ref_shr_ne `{heapGS Σ} : NonExpansive lty_ref_shr.
   Proof. solve_proper. Qed.
 
-  Global Instance lty_chan_contractive `{heapG Σ, chanG Σ} : Contractive lty_chan.
+  Global Instance lty_chan_contractive `{heapGS Σ, chanG Σ} : Contractive lty_chan.
   Proof. solve_contractive. Qed.
-  Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan.
+  Global Instance lty_chan_ne `{heapGS Σ, chanG Σ} : NonExpansive lty_chan.
   Proof. solve_proper. Qed.
 End term_types.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 579423dbe933ef825cf6bb6ab7542896a90ea3b6..52fc272e8bcb5204eb281aff190391ec1057df0d 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -12,7 +12,7 @@ From actris.logrel Require Export contexts.
 From iris.proofmode Require Import tactics.
 
 (** The semantic typing judgment *)
-Definition ltyped `{!heapG Σ}
+Definition ltyped `{!heapGS Σ}
     (Γ1 Γ2 : ctx Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
   tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗
     WP subst_map vs e {{ v, ltty_car A v ∗ ctx_ltyped vs Γ2 }})%I.
@@ -29,7 +29,7 @@ Notation "Γ ⊨ e : A" := (⊢ Γ ⊨ e : A ⫤ Γ)
   (at level 100, e at next level, A at level 200) : type_scope.
 
 Section ltyped.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Global Instance ltyped_plain Γ1 Γ2 e A : Plain (ltyped Γ1 Γ2 e A).
   Proof. rewrite /ltyped /=. apply _. Qed.
@@ -55,7 +55,7 @@ To circumvent this, we make use of the following typing judgement for values,
 that lets us type check values without requiring reduction steps.
 The value typing judgement subsumes the typing judgement on expressions,
 as made precise by the [ltyped_val_ltyped] lemma. *)
-Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
+Definition ltyped_val `{!heapGS Σ} (v : val) (A : ltty Σ) : iProp Σ :=
   tc_opaque (â–  ltty_car A v)%I.
 Instance: Params (@ltyped_val) 3 := {}.
 Notation "⊨ᵥ v : A" := (ltyped_val v A)
@@ -65,7 +65,7 @@ Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
 Arguments ltyped_val : simpl never.
 
 Section ltyped_val.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Global Instance ltyped_val_plain v A : Plain (ltyped_val v A).
   Proof. rewrite /ltyped_val /=. apply _. Qed.
@@ -79,7 +79,7 @@ Section ltyped_val.
 End ltyped_val.
 
 Section ltyped_rel.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Lemma ltyped_val_ltyped Γ v A : (⊨ᵥ v : A) -∗ Γ ⊨ v : A.
   Proof.
@@ -91,8 +91,8 @@ Section ltyped_rel.
 
 End ltyped_rel.
 
-Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
-  (∀ `{heapG Σ}, ∃ A, [] ⊨ e : A ⫤ []) →
+Lemma ltyped_safety `{heapGpreS Σ} e σ es σ' e' :
+  (∀ `{heapGS Σ}, ∃ A, [] ⊨ e : A ⫤ []) →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 6cc22f35496bba653d7a9106f21504f4956b1467..0d64cda517f5adf45a7489c9eabde90a276e5d05 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -8,7 +8,7 @@ From actris.logrel Require Export subtyping_rules term_typing_judgment operators
 From actris.channel Require Import proofmode.
 
 Section term_typing_rules.
-  Context `{heapG Σ}.
+  Context `{heapGS Σ}.
   Implicit Types A B : ltty Σ.
   Implicit Types Γ : ctx Σ.
 
diff --git a/theories/utils/compare.v b/theories/utils/compare.v
index d6c7187c6549e1edb03b058ac868d28eecfcab06..68a0ee1cb22a1e16e1e8a00915689882881fda60 100644
--- a/theories/utils/compare.v
+++ b/theories/utils/compare.v
@@ -5,17 +5,17 @@ on integers [Z].*)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 
-Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ)
+Definition cmp_spec `{!heapGS Σ} {A} (I : A → val → iProp Σ)
     (R : relation A) `{!RelDecision R} (cmp : val) : iProp Σ :=
   (∀ x x' v v',
     {{{ I x v ∗ I x' v' }}}
       cmp v v'
     {{{ RET #(bool_decide (R x x')); I x v ∗ I x' v' }}})%I.
 
-Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
+Definition IZ `{!heapGS Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
 Definition cmpZ : val := λ: "x" "y", "x" ≤ "y".
 
-Lemma cmpZ_spec `{!heapG Σ} : ⊢ cmp_spec IZ (≤)%Z cmpZ.
+Lemma cmpZ_spec `{!heapGS Σ} : ⊢ cmp_spec IZ (≤)%Z cmpZ.
 Proof.
   rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
   wp_lam. wp_pures. by iApply "HΦ".
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index ea0c67b88ea925f5a86a29788e25cc7736560f91..28c7ac18a720c9ac39be0084c12b3e7692cdf2c7 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
 
 (**  *)
-Fixpoint llist `{heapG Σ} {A} (I : A → val → iProp Σ)
+Fixpoint llist `{heapGS Σ} {A} (I : A → val → iProp Σ)
     (l : loc) (xs : list A) : iProp Σ :=
   match xs with
   | [] => l ↦ NONEV
@@ -87,7 +87,7 @@ Definition lreverse : val :=
           "l" <- !(lreverse_at "l'" (lnil #())).
 
 Section lists.
-Context `{heapG Σ} {A} (I : A → val → iProp Σ).
+Context `{heapGS Σ} {A} (I : A → val → iProp Σ).
 Implicit Types i : nat.
 Implicit Types xs : list A.
 Implicit Types l : loc.
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
index 6d154ded31844ccfc1c04a9b37fc085edb4773b3..76c38b38bbf5ed7898d402dc1ceb500cf560d710 100644
--- a/theories/utils/skip.v
+++ b/theories/utils/skip.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Import proofmode notation.
 Definition skipN : val :=
   rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
 
-Lemma skipN_spec `{heapG Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
+Lemma skipN_spec `{heapGS Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
 Proof.
   iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
   rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index 1f927178111e4a874981480509b5589d4b61f3c3..d988a225c7f284845530e952adeeca5d647fb0e1 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -51,7 +51,7 @@ Proof.
   apply IH. lia.
 Qed.
 
-Lemma switch_lams_spec `{heapG Σ} y i n ws vs e Φ :
+Lemma switch_lams_spec `{heapGS Σ} y i n ws vs e Φ :
   length vs = n →
   WP subst_map (map_string_seq y i vs ∪ ws) e {{ Φ }} -∗
   WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) w {{ Φ }} }}.
@@ -67,7 +67,7 @@ Proof.
     lookup_map_string_seq_None_lt; auto with lia.
 Qed.
 
-Lemma switch_body_spec `{heapG Σ} y xs i j ws (x : Z) edef ecase Φ :
+Lemma switch_body_spec `{heapGS Σ} y xs i j ws (x : Z) edef ecase Φ :
   fst <$> list_find (x =.) xs = Some i →
   ws !! y = Some #x →
   WP subst_map ws (ecase (i + j)%nat) {{ Φ }} -∗
@@ -82,7 +82,7 @@ Proof.
   iApply ("IH" $! i'). by simplify_option_eq. by rewrite Nat.add_succ_r.
 Qed.
 
-Lemma switch_fail_spec `{heapG Σ} vfs xs i (x : Z) (vf : val) Φ :
+Lemma switch_fail_spec `{heapGS Σ} vfs xs i (x : Z) (vf : val) Φ :
   length vfs = length xs →
   fst <$> list_find (x =.) xs = Some i →
   vfs !! i = Some vf →