Skip to content
Snippets Groups Projects
Commit 3aa2c6c8 authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris; fix for std++ change

parent b6f3e75d
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-05-17.0.463474fb") | (= "dev") }
"coq-iris" { (= "dev.2018-06-23.0.a6e581d0") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -268,13 +268,11 @@ Section stack_works.
iDestruct "Hstack" as (l'' v' xs) "[% [Hl'' [Hstack HP]]]".
iDestruct ("Hmove" with "HP") as "Hmove".
iDestruct (fupd_mask_mono with "Hmove") as "Hmove";
last iMod "Hmove" as "[HP HQ'']".
{ apply ndisj_subseteq_difference; try solve_ndisj. }
last iMod "Hmove" as "[HP HQ'']"; first solve_ndisj.
iDestruct "Hcont" as "[Hsucc _]".
iDestruct ("Hsucc" with "HP") as "Hsucc".
iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc";
last (iMod "Hsucc" as "[HQ HP]").
{ apply ndisj_subseteq_difference; try solve_ndisj. }
last (iMod "Hsucc" as "[HQ HP]"); first solve_ndisj.
iMod ("Hclose2" with "[Hl'' Hstack HP]").
{ iExists l'', v', xs; iSplit; iFrame; auto. }
iModIntro.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment