diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 00dbbb8bea6ec0be9f93c534f24282b4e25f9155..8ee195b1e5956f83dcdfe00df74bef3a04ef6b37 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-05-05.0.6f18e8cd") | (= "dev") }
+  "coq-iris" { (= "dev.2021-06-03.0.2959900d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index f8d1e5a81f94ea4b8577e5cea880ce5d0f2ee05e..e86deef4d28360e82e70907a490ba3eba17fdd57 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -4,8 +4,8 @@ From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
-Class lrustPreG Σ := HeapPreG {
-  lrust_preG_irig :> invPreG Σ;
+Class lrustPreG Σ := HeapGpreS {
+  lrust_preG_irig :> invGpreS Σ;
   lrust_preG_heap :> inG Σ (authR heapUR);
   lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
 }.
@@ -26,7 +26,7 @@ Proof.
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
   iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
     first by apply auth_auth_valid.
-  set (Hheap := HeapG _ _ _ vγ fγ).
+  set (Hheap := HeapGS _ _ _ vγ fγ).
   iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
   { iExists ∅. by iFrame. }
   by iApply (Hwp (LRustG _ _ Hheap)).
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 19b0c8214f162f9543f3d4ba93fd3194337d0d3b..62b9deff7a41ee0ffaa1b0c29b1eb2480e2209ab 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -18,7 +18,7 @@ Definition heapUR : ucmra :=
 Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
-Class heapG Σ := HeapG {
+Class heapGS Σ := HeapGS {
   heap_inG :> inG Σ (authR heapUR);
   heap_freeable_inG :> inG Σ (authR heap_freeableUR);
   heap_name : gname;
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
     qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
 
 Section definitions.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition heap_mapsto_st (st : lock_state)
              (l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -106,7 +106,7 @@ Section to_heap.
 End to_heap.
 
 Section heap.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types σ : state.
   Implicit Types E : coPset.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index efe5db0685c63c2e5525390c544a9ca52217ced3..06f2a7af62f73d19341b6089c1684637296d90cb 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -99,7 +99,7 @@ Definition try_unwrap_full : val :=
     else #2.
 
 (** 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. *)
 
 (* See rc.v for understanding the structure of this CMRA.
    The only additional thing is the [optionR (exclR unitO))], used to handle
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 93b47498c79d4bd207f36de801b2205463aac92e..9f869980a4b3e1e3e118e005ea3b9613fd6ccf8d 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class lrustG Σ := LRustG {
-  lrustG_invG : invG Σ;
-  lrustG_gen_heapG :> heapG Σ
+  lrustG_invG : invGS Σ;
+  lrustG_gen_heapG :> heapGS Σ
 }.
 
-Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
+Instance lrustG_irisG `{!lrustG Σ} : irisGS lrust_lang Σ := {
   iris_invG := lrustG_invG;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 983f27861faf86a8f818bf0fb6e51cf59d585e50..04bd55a8b4adcb8932ffb95088143ce12ea78c4c 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invG Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
+  Context `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ userE} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 3f04c378e71ab60e5d0bcf3b53777caf499f6a45..2874a6609c1d3ac135788361f3bed26b797f3bb6 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,16 +6,16 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ userE, !frac_borG Σ}
                               (φ : Qp → iProp Σ) γ κ' :=
   (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -155,7 +155,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index ace6b15d9b663ae424b64a50b209455a3dbf55de..098a789eea16d18f5aade328f1aee49487ef04a7 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,7 +26,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 908cc2e3fb5cfb3319b5c50c19c6f49ce03515d5..84ed70d6a7e44a5bacd559d0d0b2992bd6be371d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -25,17 +25,17 @@ Module Type lifetime_sig.
   Parameter static : lft.
   Declare Instance lft_intersect : Meet lft.
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ userE}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ userE}, iProp Σ.
 
   Parameter lft_tok : ∀ `{!lftG Σ userE} (q : Qp) (κ : lft), iProp Σ.
   Parameter lft_dead : ∀ `{!lftG Σ userE} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invGS Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
   Parameter idx_bor_own : ∀ `{!lftG Σ userE} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
   by a [positive] in some given infinite set. This operation converts the
@@ -53,7 +53,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftG Σ userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -172,7 +172,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : gFunctors.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E userE,
+  Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ} E userE,
     ↑lftN ⊆ E → ↑lftN ## userE →
     ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index d0f911ba82ca0af00a2826c5d5feae500143c587..62421fce0882a03907371c646ab72075010cc200 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -26,7 +26,7 @@ Definition lft_meta `{!lftG Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iP
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invG Σ, !lftG Σ userE, lft_metaG Σ}.
+  Context `{!invGS Σ, !lftG Σ 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 a905436199c911a64f3de54b9547ef790af3360c..bc460359549c54e5998f049ed61cd6905b834f65 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 4ac85ae95053f5fcd6ab1d3ca0051ca53a45152b..982cc8d51dd03bbd7a37cea2ecc832c595bc7b71 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 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 21d8c87bb04eff13dcff110f1844d22dc2a5a26e..9213e161a57308c4a801a402c2d31550b1759f7c 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 85bbedc67506a4b65651b5e75b42c0eaeac521bc..ac782d8fb49a94ee189900fa57650b94cd20b295 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 5fdd5dcd560eb4367e0ff1b59b8ddeda3ea2bc55..1a1f85e51bb8b7f791fe0beb20ddf4ac35acebea 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -80,7 +80,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftG Σ userE}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -224,7 +224,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 Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 793b7d74d9feb4f98c0f0d901a5af4e07b185bd6..1e996cd1b2cd7e7411899fdb2c51a83cbfd531c5 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index a82d3fc4770bf6d24a026664618d76b686d91e43..eaaf4991e9c154966ecdcbfbb96178ce18f14649 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{!invG Σ, !lftPreG Σ} E userE :
+Lemma lft_init `{!invGS Σ, !lftPreG Σ} E userE :
   ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
 Proof.
   iIntros (? HuserE). rewrite /lft_ctx.
@@ -20,7 +20,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index f8502152a37af379eac16b89ba94bb97db92daf1..a77e597add827bd730acd9aff26c9c478052044a 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 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 fa964406411cbde05f390652141b692c40617883..fec690bc433258691da17a500e93829a8685d17b 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ userE, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 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 Σ userE, !na_invG Σ}
+  Context `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   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 3f3c144a7e3512ab48f342a1f4cd98e7515f07c7..f869d85e283db9811ee4cda5dcf8af5ce521dfb9 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 Σ lft_userE}.
+  Context `{!invGS Σ, !lftG Σ 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 Σ lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.