diff --git a/opam b/opam index 2a1f61e764f81ee07c48f77558d93d4971f8094d..1a76efef56a6f4c04d334709e40bcb7072b12116 100644 --- a/opam +++ b/opam @@ -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") } ] diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v index a58480332962933c1cccfcd139da3003f23015fe..77693af713ffe55aab63924a86f5baffff15b8fe 100644 --- a/theories/examples/map_reduce.v +++ b/theories/examples/map_reduce.v @@ -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 /=.