bump Iris; fix for std++ rename

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

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.

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 :

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.