Skip to content
Snippets Groups Projects
Commit 9a1d75a2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris (iFrame).

parent 536f5d38
No related branches found
No related tags found
No related merge requests found
Pipeline #97929 passed
......@@ -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}%"]
......
......@@ -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 %->.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment