diff --git a/opam b/opam
index 27f078c2779fc46c31ef9a6aaadbb861c749af6b..9c3d0ce5b20c331482ec8e5e03eb91a54b35eefb 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-11-11.0.60647cc2") | (= "dev") }
+  "coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index bd164ce8861247fa491240bf05a456d5f9d2696a..3fa9066e3cd61147e94ee3d890d5a62b4d57925f 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -181,7 +181,7 @@ Proof.
         solve_ndisj. by rewrite lookup_fmap EQB.
       iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
       { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
-      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/typing/soundness.v b/theories/typing/soundness.v
index 84f4c4d382bb686c605dcc18151cce71166b005b..6157b9a8542db5cd9e35df64332ecdf384bb6439 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -38,7 +38,7 @@ Section type_soundness.
     iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     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 big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }