From 4eae63762b0ec111aa44c826abb8c93bd7c3b735 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Apr 2023 10:50:47 +0200
Subject: [PATCH] Remove ad-hoc (old) version of `multiset_solver`.

---
 theories/hocap/contrib_bag.v | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/theories/hocap/contrib_bag.v b/theories/hocap/contrib_bag.v
index 56573c38..d0c6b779 100644
--- a/theories/hocap/contrib_bag.v
+++ b/theories/hocap/contrib_bag.v
@@ -76,11 +76,6 @@ Section proof.
     iNext. iExists _; iFrame.
   Qed.
 
-  Local Ltac multiset_solver :=
-    intro;
-    repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union);
-    (lia || naive_solver).
-
   Lemma popBag_spec γb γ x X :
     {{{ bagM γb γ x ∗ bagPart γ 1 X }}}
        popBag b x
-- 
GitLab