From ef59f1b0066ca933e4f24673a9079361bd36d3ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Sep 2019 12:58:38 +0200
Subject: [PATCH] Fix for recent std++.
---
theories/examples/map.v | 2 +-
theories/examples/map_reduce.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 76b6589..5cafc7f 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -185,7 +185,7 @@ Section map.
iApply ("HΦ" $! (ys' ++ map x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
- rewrite (comm disj_union) gmultiset_elements_disj_union.
+ 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.
Qed.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 6d872ce..97f5853 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -160,7 +160,7 @@ Section mapper.
rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
- rewrite (comm disj_union) gmultiset_elements_disj_union.
+ 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.
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 //.
- rewrite (comm disj_union) gmultiset_elements_disj_union.
+ 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.
Qed.
--
GitLab