From 550633bfc4f5957d01f0a744b534be9637790471 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Mar 2021 08:46:57 +0100
Subject: [PATCH] Bump std++.
---
opam | 2 +-
theories/examples/map_reduce.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 2a1f61e..1a76efe 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 a584803..77693af 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 /=.
--
GitLab