diff --git a/opam b/opam
index e10cbb87410ee8bb8b5be7dd84ee306a7409f8c0..b90c4973746c03aaa8323ff57da37164532a2e7b 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-02-15.1.a9cd56f7") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-02-25.0.388769e1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index bc673b3d7ece76961f3ea4ac6fd496dc4d61ec38..23036e9161169fa6bbb5aba40ff9b20eb5cbaedb 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -20,7 +20,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 a97757f1a3b3344f9154229ad251be5c6419dc77..cfe937963a089142ca6c1dc4662b0639d0d3dd81 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -681,7 +681,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.