From b7718c90ebf5463d250fcd0e34eb0b4f28ff2cd2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 Feb 2020 11:58:41 +0100
Subject: [PATCH] bump Iris; fix for std++ rename
---
opam | 2 +-
theories/lang/lifting.v | 2 +-
theories/typing/cont.v | 2 +-
theories/typing/type.v | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/opam b/opam
index 24c79f67..50566837 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 a174b301..3b0aa996 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 1011aa94..12a6374d 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 b563e6eb..f37ede51 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.
--
GitLab