bump GPFSL; std++ rename fix

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}%"]

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 :

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.