diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 0344def4df38c37c63f3ce99b5d5003cdee46ab6..03d19f9734119c2cb697c8f45349b8c8817231b4 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-05-27.0.193d6230") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-06-03.0.d0c552b5") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 3513d9943a31a3e1f66cf4b52b301275dd94f4a4..e0d685a2d0d3fa6fba99b7c1f3926149240d8364 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,12 +9,12 @@ Set Default Proof Using "Type".
    created, and the payload could be weakened without synchronizing
    with the end of the lifetime (remember that the underlying payload
    is not necessarily independent of the view for views older than V). *)
-Definition at_bor `{!invG Σ, !lftG Σ Lat userE} κ N (P : monPred _ _) : monPred _ _ :=
+Definition at_bor `{!invGS Σ, !lftG Σ Lat userE} κ N (P : monPred _ _) : monPred _ _ :=
   (∃ i, ⌜N ## lftN⌝ ∗ &{κ,i}P ∗ ⎡inv N (∃ V', idx_bor_own i V')⎤)%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   Global Instance at_bor_ne κ n N : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6c112d31666674d9122bac43bf9ddf78fd43a411..997b4a726bfed60191d230f7dbaee2330d6f09b8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}
                               (φ : Qp → monPred _ _) (V0 : Lat ) γ κ : monPred _ _:=
   (∃ (qfresh : Qp) (qdep qused : option Qp),
       (* We divide the 1 fraction into 3 parts... *)
@@ -24,7 +24,7 @@ Local Definition frac_bor_inv `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}
          enough fractions of the lifetime in deposit. *)
       ⎡own γ (qfresh ⋅? qused)⎤)%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
+Definition frac_bor `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
         (φ : Qp → monPred _ _) : monPred _ _ :=
   (* First, we close up to a bunch of things: iff, lifetime inclusion and view
      inclusion. We also existentially bind γ, the ghost name of receipts. *)
@@ -38,7 +38,7 @@ Definition frac_bor `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}.
+  Context `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}.
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 3ca7be4bc2a6c61bb71e91742fdb6161344accb5..e77f22f6ad0f353df96a3598f493f00456d0f76b 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -29,7 +29,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E `{LatBottom Lat} :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 04373ae202908a51167ee7da769719df95997129..9f1410507b1e2bdcc2352076170ec67852115d11 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -31,24 +31,24 @@ Module Type lifetime_sig.
   Section defs.
   Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ Lat userE}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ Lat userE}, iProp Σ.
 
   Parameter lft_tok : ∀ `{!lftG Σ Lat userE} (q : Qp) (κ : lft), monPred Σ Lat.
   Parameter lft_dead : ∀ `{!lftG Σ Lat userE} (κ : lft), monPred Σ Lat.
 
   Parameter lft_incl :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ κ' : lft), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ κ' : lft), monPred Σ Lat.
   Parameter bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
 
   Parameter bor_idx : Type.
   Parameter idx_bor_own : ∀ `{!lftG Σ Lat userE} (i : bor_idx), monPred Σ Lat.
   Parameter idx_bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (i : bor_idx) (P : monPred Σ Lat),
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (i : bor_idx) (P : monPred Σ Lat),
       monPred Σ Lat.
 
   Parameter in_at_bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
   End defs.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
@@ -68,7 +68,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -224,7 +224,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : latticeT → gFunctors.
   Global Declare Instance subG_lftPreG Lat Σ : subG (lftΣ Lat) Σ → lftPreG Σ Lat.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ Lat} E userE,
+  Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ Lat} E userE,
       ↑lftN ⊆ E → ↑lftN ## userE →
       ⊢ |={E}=> ∃ _ : lftG Σ Lat userE, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index f6d677a67fdfc3b6a1426dc1f6b2eb29c955c749..331d3cf227cedf1de6bbb9f61c9c7d624cc09efe 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -26,7 +26,7 @@ Definition lft_meta `{!lftG Σ Lat userE, lft_metaG Σ} (κ : lft) (γ : gname)
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invG Σ, !lftG Σ Lat userE, lft_metaG Σ}.
+  Context `{!invGS Σ, !lftG Σ Lat userE, lft_metaG Σ}.
 
   Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
   Proof. apply _. Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 8f60ff1943ee82df27ce2b0dd92e832c09ff7e26..234e65f164d8496b0a3b2d1bd3ab2cc46edb044b 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import csum auth excl frac gmap agree gset.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 (* Internal helper lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 9b10f6b51c84d852ae6558790319aa9fdbd8982b..3c491d1c4ff910b839e46a1a41870dc0cc53afc7 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index ef7f0cd1ed6e42b50eccc719c7e5018907f0caab..8b7f5ced3c6b1ee0773ceff003bd54ae9d3c5900 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -28,7 +28,7 @@ Proof.
 Qed.
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index aaffe5408f4119cc0802bb06d0dcffec781573ea..548df8b33670c46b07e6c4919d9032247a90234a 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -22,7 +22,7 @@ Instance subG_stsΣ Lat Σ : subG (boxΣ Lat) Σ → boxG Lat Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.
-  Context `{invG Σ, boxG Lat Σ} (N : namespace).
+  Context `{invGS Σ, boxG Lat Σ} (N : namespace).
   Notation iProp := (iProp Σ).
   Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
@@ -54,7 +54,7 @@ Instance: Params (@slice) 6 := {}.
 Instance: Params (@box) 6 := {}.
 
 Section box.
-Context `{invG Σ, boxG Lat Σ} (N : namespace).
+Context `{invGS Σ, boxG Lat Σ} (N : namespace).
 
 Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 Implicit Types P Q : monPred.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index d228d2ad678e26629159370fbc07ae5bae439017..d4ed860eb42703647822c87428c2a7df751a94f8 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) (Vs : lft → Lat) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 31feccb7c60db67bbd9d0b0e0b6550c4132e71f0..7a4c5972bf6d22b230faa4baf0ec6884fe305186 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -84,7 +84,7 @@ Definition to_borUR {Lat} : gmap slice_name (bor_state Lat) → borUR Lat :=
   fmap Excl.
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   Notation iProp := (iProp Σ).
   Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
@@ -236,7 +236,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Notation iProp := (iProp Σ).
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index cb4d43b105f9103f621dfec63a3d897b79c840d2..334b4e9611b6f7e7de54dfb3132109fd47863665 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat bot}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/in_at_borrow.v b/theories/lifetime/model/in_at_borrow.v
index a3459a3936d1456abfbf3e3108758e4553befafc..a7677e2e32a2dff40d0e54970e55ac1e4f9f487a 100644
--- a/theories/lifetime/model/in_at_borrow.v
+++ b/theories/lifetime/model/in_at_borrow.v
@@ -16,7 +16,7 @@ Set Default Proof Using "Type".
 
 Definition in_atN : namespace := lftN .@ "in_at".
 
-Definition in_at_bor `{invG Σ, lftG Σ Lat userE} κ P :=
+Definition in_at_bor `{invGS Σ, lftG Σ Lat userE} κ P :=
     (∃ P' i, (κ ⊑ (i.1))
                ∗ ▷ □ (P' ↔ P) ∗ ⎡slice borN (i.2) P'⎤
                ∗ ⎡inv in_atN (∃ V', idx_bor_own i V')⎤)%I.
@@ -24,7 +24,7 @@ Notation "&in_at{ κ }" := (in_at_bor κ) (format "&in_at{ κ }") : bi_scope.
 Instance in_at_bor_params : Params (@in_at_bor) 5 := {}.
 
 Section in_at.
-Context `{invG Σ, lftG Σ Lat userE}.
+Context `{invGS Σ, lftG Σ Lat userE}.
 
 Global Instance in_at_bor_ne κ n : Proper (dist n ==> dist n) (in_at_bor κ).
 Proof. solve_proper. Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1e54efe6ed7dca34f5a1021ffaa53f3328e509e8..71c6bc1e6836b5e1e067e73f690bd0e9e674a977 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -5,7 +5,7 @@ From lrust.lifetime.model Require Export definitions boxes.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{!invG Σ, !lftPreG Σ Lat} E userE :
+Lemma lft_init `{!invGS Σ, !lftPreG Σ Lat} E userE :
   ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ Lat userE, lft_ctx.
 Proof.
   iIntros (? HuserE). rewrite /lft_ctx.
@@ -19,7 +19,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name (bor_state Lat)) i s :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 6a20e460ff37e25b9c28fc9f55b78b7365e92f86..9bda0563b2ff5bfdf657703c9029ea1b1da2fe8a 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -29,7 +29,7 @@ Proof.
 Qed.
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index bf16113dc361f263067ef7250b16fe63350ffc14..a5ed5cd9d84c99c412c2844a6a3bf95bc5ac447c 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From gpfsl.logic Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ View userE, na_invG View bot Σ}
+Definition na_bor `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : monPred _ _) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invG Σ, !lftG Σ View userE, na_invG View bot Σ}
+  Context `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
           (tid : na_inv_pool_name) (N : namespace).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 03f38776ec8f8d5e3fc775791cd296edf8f90153..720b53d9143a4663ad44c247df4e425e6f917416 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{!invG Σ, !lftG Σ view_Lat lft_userE}.
+  Context `{!invGS Σ, !lftG Σ view_Lat lft_userE}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ view_Lat lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ view_Lat lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.