diff --git a/opam b/opam
index 3916574c661ca0a2e3486b3dce6ea1c02e3c45e2..0aaf5e4e32e7b1865c4bcec7fa40535036292bcd 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2020-02-12.0.119dcc0b") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-02-15.1.a9cd56f7") | (= "dev") }
 ]
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 5da27ef6803dafe820f9bd19b06d8274d9008c5d..1ee27269f2fa91fd57d5b5511161f6496f2cb620 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -44,7 +44,7 @@ Section na_bor.
   Proof.
     iIntros (???) "#LFT#HP Hκ Hnaown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
+    iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
     iMod (idx_bor_acc_sync with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
     iIntros "{$HP $Hnaown} !> HP Hnaown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 6b25d86c69c92231d6e014754e28b81b013a7d3c..3cc26d38b6b34a14743fbc1ccf647d9d0ad911b8 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -125,7 +125,7 @@ Section arc.
     iMod (inv_alloc arc_endN with "[H]") as "#INV".
     { rewrite -embed_or. iNext. by iApply "H". }
     iIntros "!> !# Hν".
-    iMod (inv_open with "INV") as "[[H†|[>$ Hvs]] Hclose]"; [set_solver|..].
+    iMod (inv_acc with "INV") as "[[H†|[>$ Hvs]] Hclose]"; [set_solver|..].
     { iDestruct "H†" as (?) ">H†".
       iDestruct (lft_tok_dead_subj with "Hν [H†]") as "[]".
       rewrite monPred_subjectively_unfold. by iExists _. }
@@ -176,7 +176,7 @@ Section arc.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
           with "[Hpbown]") as "#Hinv"; [by iLeft; iFrame|].
     iIntros "!> !# * % Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
@@ -315,7 +315,7 @@ Section arc.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
           with "[Hpbown]") as "#Hinv"; first by iLeft; iFrame.
     iIntros "!> !# * % Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index b0ffc6abbbfe7321ff6f6b3342771532e23957d4..35a255fb617b8c0e65444207395c07c446a546d8 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -144,7 +144,7 @@ Section rc.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
           with "[Hpbown]") as "#Hinv"; [by iLeft; iFrame|].
     iIntros "!> !#" (F q' ?) "Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
@@ -286,7 +286,7 @@ Section code.
         auto 10 with iFrame.
     - iDestruct "Hown" as (γ ν q) "(#Hpersist & Htok & Hν1)".
       iPoseProof "Hpersist" as (ty') "(Hincl & Hinv & _ & #Hνend)".
-      iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+      iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
       iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
         %option_included _]%prod_included [Hval _]]%auth_both_valid.
@@ -345,7 +345,7 @@ Section code.
           rewrite Hincls. iFrame. iSplitL "Hty".
           { iDestruct "Hty" as (vl) "[??]". iExists _. iFrame. by iApply "Hinclo". }
           iIntros "!> Hna". iClear "Hνend". clear q' Hqq' weak Hval.
-          iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+          iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
           iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
           iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
             %option_included _]%prod_included [Hval _]]%auth_both_valid.
@@ -415,7 +415,7 @@ Section code.
     iModIntro. wp_let. wp_op. rewrite shift_loc_0.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
@@ -474,7 +474,7 @@ Section code.
     iModIntro. wp_let. wp_op.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
@@ -579,7 +579,7 @@ Section code.
     iModIntro. wp_let. wp_op. rewrite shift_loc_0.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index e5ef1983416ea547d5656c6a920091d51858911e..b91f07af1757ecbee8702e136fc0f482bf3ad6e1 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -41,7 +41,7 @@ Section weak.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I with "[Hpbown]") as "#Hinv";
       [by iLeft; iFrame|].
     iIntros "!> !#" (F q' ?) "Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
@@ -160,7 +160,7 @@ Section code.
     iModIntro. wp_let. wp_op. rewrite shift_loc_0.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hwtok") as
@@ -263,7 +263,7 @@ Section code.
     iModIntro. wp_let. wp_op.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
@@ -329,7 +329,7 @@ Section code.
     iAssert (∃ wv : Z, (l' +ₗ 1) ↦ #wv ∗ ((l' +ₗ 1) ↦ #(wv + 1) ={⊤}=∗
                na_own tid ⊤ ∗ (q / 2).[α] ∗ ⎡own γ weak_tok⎤))%I
       with "[> Hna Hα1]" as (wv) "[Hwv Hclose2]".
-    { iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+    { iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
       iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
@@ -403,7 +403,7 @@ Section code.
       with "[>Hna Hwtok]" as (wv) "[Hlw [(% & Hna & H)|[% Hclose]]]".
     { iPoseProof "Hpersist" as (ty') "([>Hszeq _] & Hinv & _ & _)".
       iDestruct "Hszeq" as %Hszeq.
-      iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
+      iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
           %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 18cf8124459ddcaa2005211c91aa88b9ee1c18bb..092d93841a79e614e2248327506c346f64732f8d 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -37,7 +37,7 @@ Section util.
           with "[Hpbown]") as "#Hinv".
     { iModIntro. eauto. }
     iIntros "!> !# * % Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - rewrite -(Qp_div_2 q).
       iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
@@ -68,7 +68,7 @@ Section util.
           with "[Hpbown]") as "#Hinv".
     { iModIntro. auto. }
     iIntros "!> !# * % Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
+    iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - rewrite -(Qp_div_2 q).
       iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".