From aefab58b13e35618badf3bc0015b512b89123434 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Jun 2021 16:08:23 +0200
Subject: [PATCH] update dependencies

---
 opam                                          |  2 +-
 theories/channel/channel.v                    |  6 ++--
 theories/channel/proofmode.v                  | 10 +++----
 theories/examples/basics.v                    |  2 +-
 theories/examples/equivalence.v               |  2 +-
 theories/examples/list_rev.v                  |  2 +-
 theories/examples/map_reduce.v                |  2 +-
 theories/examples/par_map.v                   |  2 +-
 theories/examples/pizza.v                     |  2 +-
 theories/examples/rpc.v                       |  2 +-
 theories/examples/sort.v                      |  2 +-
 theories/examples/sort_br_del.v               |  2 +-
 theories/examples/sort_fg.v                   |  2 +-
 theories/examples/subprotocols.v              |  2 +-
 theories/examples/swap_mapper.v               |  2 +-
 theories/logrel/examples/choice_subtyping.v   |  2 +-
 .../logrel/examples/compute_client_list.v     |  2 +-
 theories/logrel/examples/compute_service.v    |  2 +-
 theories/logrel/examples/mapper.v             |  2 +-
 theories/logrel/examples/mapper_list.v        |  2 +-
 theories/logrel/examples/pair.v               |  2 +-
 theories/logrel/examples/par_recv.v           |  4 +--
 theories/logrel/examples/rec_subtyping.v      |  2 +-
 theories/logrel/lib/list.v                    |  8 ++---
 theories/logrel/lib/mutex.v                   |  8 ++---
 theories/logrel/lib/par_start.v               |  2 +-
 theories/logrel/napp.v                        |  2 +-
 theories/logrel/operators.v                   |  4 +--
 theories/logrel/session_typing_rules.v        |  2 +-
 theories/logrel/subtyping_rules.v             |  2 +-
 theories/logrel/term_types.v                  | 30 +++++++++----------
 theories/logrel/term_typing_judgment.v        | 14 ++++-----
 theories/logrel/term_typing_rules.v           |  2 +-
 theories/utils/compare.v                      |  6 ++--
 theories/utils/llist.v                        |  4 +--
 theories/utils/skip.v                         |  2 +-
 theories/utils/switch.v                       |  6 ++--
 37 files changed, 76 insertions(+), 76 deletions(-)

diff --git a/opam b/opam
index fc9bcb0..bb48e99 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 99e90d5..9e1380a 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 a709199..8f4294b 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 62a1972..29b7e32 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 73d5c35..9bb81a5 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 a851ea0..0f65fc9 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 3f7832d..9c3ae33 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 661369f..a4cd7c7 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 75d9d7f..6180e22 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 eefed48..45332c6 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 e5df3a0..03f9510 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 c628d3e..10ec01f 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 599c12d..f657fad 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 57030fd..c6842d4 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 22adfcd..42446ee 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 68d3fbe..09e72f7 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 4e675a8..97679f3 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 1495297..38ec165 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 55290e0..0f46546 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 7c57be0..cd7c109 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 34228f1..6f7a6a5 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 3f8e654..81e56a4 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 e1abf8a..f536f57 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 4ee66b8..3f5e646 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 47b1065..9e2d515 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 5f0e2e2..bdb1127 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 ecbda68..bccdac6 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 7abfb4f..267f47e 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 1a2b24d..25b5c3a 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 d87b685..321edfd 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 99dd882..615562c 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 579423d..52fc272 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 6cc22f3..0d64cda 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 d6c7187..68a0ee1 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 ea0c67b..28c7ac1 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 6d154de..76c38b3 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 1f92717..d988a22 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 →
-- 
GitLab