Commit 6f833876 authored by Ralf Jung's avatar Ralf Jung
Browse files

update Iris so that we can use iSplit again instead of iSplitL

parent 56a695de
Pipeline #8502 passed with stage
in 27 minutes and 34 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-08.0.7af1bbd3") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-09.1.c2b96095") | (= "dev") }
]
......@@ -1308,7 +1308,7 @@ Tactic Notation "refine_unbind" constr(K) :=
}
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ iFrame "Hown". iFrame "Hheap". iFrame "Hscheap".
repeat iSplitL; iPureIntro; eauto with ndisj. }
repeat iSplit; iPureIntro; eauto with ndisj. }
iApply wp_wand_l. iFrame "Hwp".
iIntros "!#". iIntros (v) "Hpre".
iDestruct "Hpre" as (l c) "(%&Hleft&Hright&Hown)".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment