From afe73d886b07dcbac73e4235554f8a1427d60eee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 00:44:42 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/examples/map_reduce.v | 4 ++--
theories/examples/par_map.v | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/opam b/opam
index c99b251..96e5496 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-07-19.3.ce8bd0c6") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2021-07-26.8.eb05e835") | (= "dev") }
]
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 62d5dfc..8f0f97c 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -160,7 +160,7 @@ Section mapper.
iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
- -?gmultiset_elem_of_singleton_subseteq //.
+ ?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
Qed.
@@ -266,7 +266,7 @@ Section mapper.
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)
- -?gmultiset_elem_of_singleton_subseteq //.
+ ?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
by rewrite right_id_L !assoc_L.
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index a4cd7c7..d9f6f80 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -187,7 +187,7 @@ Section map.
iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
iApply ("HΦ" $! (ys' ++ map x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
- -?gmultiset_elem_of_singleton_subseteq //.
+ ?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
+ by rewrite -assoc_L.
--
GitLab