diff --git a/opam b/opam
index aba89f116a0831b167921537791bd3f6bcc0f7f4..9b7b45e1cca09a38ad0a1a8534bba28ca0237e29 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.2019-11-07.3.ed0b4138") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-11-21.0.16013a13") | (= "dev") }
 ]
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index fcfba6541bd471d2034ba339317e6e63489ffb2d..9a15a20daab4a7b62c286cce7a9ea059c4733485 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -87,7 +87,7 @@ Module Type lifetime_sig.
 
   Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
   Global Declare Instance bor_contractive κ : Contractive (bor κ).
-  Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+  Global Declare Instance bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (bor κ).
   Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
   Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
   Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index ac0ae54f868a29a4d85cb2ee214257207cd8b78e..02dc8eee40f6c82f6a6260f2c02379d280f007e9 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -152,7 +152,8 @@ Proof.
   iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
   { iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct "H†" as (V) "H†".
-    iDestruct (lft_tok_dead $! (Vtok⊔V) with "Htok H†") as "[]". }
+    set (V' := Vtok ⊔ V).
+    iDestruct (lft_tok_dead $! V' with "Htok H†") as "[]". }
   rewrite [in _ Vκ]lft_inv_alive_unfold.
   iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
   iMod (bor_open_internal with "Hs Halive Hbor Htok") as (V) "(% & Halive & Hf & HP)".
@@ -250,7 +251,8 @@ Proof.
   { iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (monPred_in_intro with "Htok") as (Vtok) "[_ Htok]".
     iDestruct "H†" as (V) "H†". iAssert ⎡False⎤%I as %[]. iModIntro.
-    iApply (lft_tok_dead $! (Vtok⊔V) with "Htok H†"). }
+    set (V' := Vtok ⊔ V).
+    iApply (lft_tok_dead $! V' with "Htok H†"). }
   rewrite [in _ Vκ]lft_inv_alive_unfold.
   iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
   iCombine "Hbor Htok" as "HborHtok".
@@ -282,7 +284,7 @@ Proof.
     as %[EQB%to_borUR_included _]%auth_both_valid.
   iDestruct (slice_delete_empty _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
     by rewrite lookup_fmap EQB.
-  iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
+  iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
   iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
   { apply auth_update. etrans.
     - apply delete_singleton_local_update, _.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index e4b23b6c00ee6457580835ea227fad0534c3fde3..45153a63013bbf3cc0cca5d834d4d1a84e9f6dba 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -27,7 +27,8 @@ Proof.
   { iIntros (i s HBI). rewrite (big_sepM_lookup _ B) //.
     destruct s as [V|q|κ']; rewrite /bor_cnt; [iExists _; by iSplit| |].
     { iDestruct "HB" as "[_ HB]". iDestruct "Hκ" as (Vκ) "Hκ".
-      iDestruct (lft_tok_dead $! (Vtok⊔Vκ) with "HB Hκ") as "[]". }
+      set (V' := Vtok ⊔ Vκ).
+      iDestruct (lft_tok_dead $! V' with "HB Hκ") as "[]". }
     iDestruct "HB" as "(% & % & Hcnt)". iDestruct (own_cnt_auth with "HI Hcnt") as %?.
     iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; [by apply HK|].
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R Vinh) "(_ & _ & Hcnt' & _)".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 5fb4dde07b29102a4169c0d346543a180dc19ea9..82d427ac4740c40094859c0f83df7d5ae1f2a0cc 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -335,7 +335,7 @@ Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
 Proof. solve_proper. Qed.
 Global Instance bor_contractive κ : Contractive (bor κ).
 Proof. solve_contractive. Qed.
-Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+Global Instance bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (bor κ).
 Proof. apply (ne_proper _). Qed.
 
 (*** PersistentP and TimelessP and instances  *)
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e7c06d9299a85d3a583e01924987d108842fc97b..771070fdc805ed16859837f1d00276eb84f4ff59 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -193,7 +193,7 @@ Proof.
   iCombine "HP' HV'" as "HP'V'".
   iDestruct (monPred_in_intro with "HP'V'") as (V) "(HV & HP'V & %)".
   iMod (raw_bor_unnest Vκ with "[HP'V] [$HI $Hinvκ] Hidx Hs [Hbox H● HB] [Hvs]")
-    as (Pb'') "HH"; [solve_ndisj|try done..]; [| | |].
+    as (Pb'') "HH"; [solve_ndisj|done|done|done|done| | | |].
   { iIntros "!>!>!>". by iDestruct  "HP'V" as "#HP'V". }
   { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
     iExists (delete i' B). rewrite -fmap_delete. iFrame.
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 57af8956dde3d30f213e1420774b51118de88eb4..6fb45cfdf85ac148913d604d3ad713c744d0c9d9 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -33,7 +33,7 @@ Proof.
   iDestruct "Hl" as (v) "[>Hl P]".
   set Q' : time → gname → vProp :=
     (λ t γ, Q t v γ ∗ GPS_SWReader l t s v γ)%I.
-  iMod (GPS_SWRaw_Init_vs_strong IP l IPC true _ _ Q' with "Hl [HP P]")
+  iMod (GPS_SWRaw_Init_vs_strong IP l IPC true _ s Q' with "Hl [HP P]")
     as (γ t) "[Inv [Q R]]".
   { iIntros (t γ) "W". iDestruct (GPS_SWWriter_Reader with "W") as "#$".
     by iApply ("HP" with "P W"). }
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 2ccbebc0cfdc6a8e9ef6dcbe7bf47fb50ace3b0d..3e282b53ed3a4293e92457df7da1cc55c0a8f6c0 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -44,7 +44,7 @@ Section type_soundness.
     iMod na_alloc as (tid2) "Htl". set (Htype := TypeG _ _ _ _ _).
     set (tid := {| tid_na_inv_pool := tid2; tid_tid := tid1 |}).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
-    { iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []");
+    { iApply (Hmain Htype [] [] $! tid with "LFT [] Htl [] []");
         by rewrite /elctx_interp /llctx_interp ?tctx_interp_nil. }
     clear Hrtc Hmain main. iIntros (main) "(Htl & _ & Hmain & _)".
     iDestruct "Hmain" as (?) "[EQ Hmain]".