From 2c66ea03c1cdb87e483c2111fa6ae90453141262 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Apr 2023 18:40:30 +0200
Subject: [PATCH] Use multiset singleton for multisets.
---
theories/hocap/shared_bag.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/hocap/shared_bag.v b/theories/hocap/shared_bag.v
index c9911f11..cd202660 100644
--- a/theories/hocap/shared_bag.v
+++ b/theories/hocap/shared_bag.v
@@ -52,7 +52,7 @@ Section proof.
{ iModIntro. iIntros (Y) "[Hb1 HP]".
iInv NI as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
- iMod (bag_contents_update b ({[v]} ⊎ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
+ iMod (bag_contents_update b ({[+ v +]} ⊎ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iFrame. iApply "Hcl".
iNext. iExists _; iFrame.
rewrite big_sepMS_singleton. iFrame. }
--
GitLab