From d6fb18080144aae68794dc90bcedc4d60d7a5b78 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Feb 2024 19:59:22 +0100
Subject: [PATCH] Bump Iris (iFrame).
---
coq-actris.opam | 2 +-
theories/examples/list_rev.v | 3 +--
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/coq-actris.opam b/coq-actris.opam
index d79e967..0a6f3ae 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2024-02-02.1.b30c53e2") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 70d0ade..17cbdcd 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -39,8 +39,7 @@ Section list_rev_example.
+ iExists []. eauto.
+ iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
- iExists (v::vs). iFrame.
- iExists v, lcons. eauto with iFrame.
+ iExists (v::vs). by iFrame.
- iDestruct 1 as (vs) "[Hvs HIT]".
iInduction xs as [|x xs] "IH" forall (l vs).
+ by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
--
GitLab