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

Bump std++.

parent 626784fd
No related branches found
No related tags found
No related merge requests found
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris-heap-lang" { (= "dev.2021-01-26.0.a26cf167") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2021-03-12.0.5011fae3") | (= "dev") }
]
......@@ -265,7 +265,7 @@ Section mapper.
wp_smart_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
iPureIntro. rewrite (gmultiset_disj_union_difference {[ (i,ys) ]} Y)
-?gmultiset_elem_of_singleton_subseteq //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
......
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