From de52d5d02612630c15f62b7f3efa937867649a97 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 Feb 2020 14:02:10 +0100
Subject: [PATCH] bump GPFSL; std++ rename fix
---
opam | 2 +-
theories/typing/cont.v | 2 +-
theories/typing/type.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index e10cbb87..b90c4973 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 bc673b3d..23036e91 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 a97757f1..cfe93796 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.
--
GitLab