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

update Iris

parent e746c3cc
No related branches found
No related tags found
No related merge requests found
Pipeline #38898 failed
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 946ba572
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [ depends: [
"coq-iris-heap-lang" { (= "dev.2020-11-11.4.e34f8ac7") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2020-11-26.2.03b317f4") | (= "dev") }
] ]
theories/utils/switch.v
+ 1
− 0
View file @ 946ba572
...@@ -60,6 +60,7 @@ Proof. ...@@ -60,6 +60,7 @@ Proof.
iInduction vs as [|v vs] "IH" forall (i ws); csimpl. iInduction vs as [|v vs] "IH" forall (i ws); csimpl.
{ rewrite left_id_L. { rewrite left_id_L.
iApply (wp_wand with "H"); iIntros (v) "H". by iApply wp_value. } iApply (wp_wand with "H"); iIntros (v) "H". by iApply wp_value. }
pose proof @pure_exec_fill.
wp_pures. iApply wp_bind. wp_pures. iApply wp_bind.
iEval (rewrite -subst_map_insert insert_union_singleton_l). iEval (rewrite -subst_map_insert insert_union_singleton_l).
iApply "IH". rewrite assoc_L insert_union_singleton_r // iApply "IH". rewrite assoc_L insert_union_singleton_r //
......
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