diff --git a/opam b/opam
index 24c79f67bd25a61cc28557ac13c9fe86e567ad65..50566837caee5af7e78ab1f63bb1bb951249cdc5 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-02-18.0.3b0457d4") | (= "dev") }
+  "coq-iris" { (= "dev.2020-02-25.0.55283d57") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index a174b301a376e0dd131a15ce35f3f4f2f0a25606..3b0aa996b1ef3a8040f57b2ec5c4817d7ac439e9 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -369,7 +369,7 @@ Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
              WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
 Proof.
-  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
+  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_to_vec Ql).
   generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
   iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
   iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 1011aa9412071ff20563a91c0ab864cedb2b519a..12a6374d6596165566e4750847b3071bac5f3c4c 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -21,7 +21,7 @@ Section typing.
     iSpecialize ("HC" with "[]"); first done.
     assert (args = of_val <$> argsv) as ->.
     { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
-    rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
+    rewrite -{3}(vec_to_list_to_vec argsv). iApply ("HC" with "Hna HL HT").
   Qed.
 
   Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b563e6ebbe0e05238d694f52ef4f9d289a30571b..f37ede510ebd9f5dd067dcd3d2e855d2e980025d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -678,7 +678,7 @@ Section type_util.
     iSplit.
     - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]".
       iDestruct (ty_size_eq with "Hown") as %<-.
-      iExists (list_to_vec vl). rewrite vec_to_list_of_list. iFrame.
+      iExists (list_to_vec vl). rewrite vec_to_list_to_vec. iFrame.
     - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]". eauto with iFrame.
   Qed.