From 1476c05cbe82d2cf2a957b4bf9ae59f9825c0198 Mon Sep 17 00:00:00 2001
From: Andrej Dudenhefner <31094379+mrhaandi@users.noreply.github.com>
Date: Tue, 12 Jul 2022 12:34:46 +0200
Subject: [PATCH] improved auto goal selection (see coq/#16293) (#43)

---
 Util/Multiset/MultisetListOrder.v | 6 +++---
 Util/Multiset/MultisetTheory.v    | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Util/Multiset/MultisetListOrder.v b/Util/Multiset/MultisetListOrder.v
index 20157cfd..3e4e867c 100644
--- a/Util/Multiset/MultisetListOrder.v
+++ b/Util/Multiset/MultisetListOrder.v
@@ -436,10 +436,10 @@ Module MultisetListOrder (ES : Eqset_dec).
       subst; simpl; simpl in H1.
       unfold mult, MultisetLT, transp; simpl.
       constructor 1 with (X := {{a'}}) (Y :={{a}}) (Z := (list2multiset l));
-        auto with multisets.
-      unfold insert; simpl; auto with multisets.
+        [auto with multisets|..].
+      unfold insert; simpl.
       rewrite union_comm; auto with multisets.
-      unfold insert; simpl; auto with multisets.
+      unfold insert; simpl.
       rewrite union_comm; auto with multisets.
       intros y Hy; assert (HY : y =A= a).
       apply (member_singleton Hy).
diff --git a/Util/Multiset/MultisetTheory.v b/Util/Multiset/MultisetTheory.v
index 600d85f5..cd950b77 100644
--- a/Util/Multiset/MultisetTheory.v
+++ b/Util/Multiset/MultisetTheory.v
@@ -1316,7 +1316,7 @@ Module Multiset (MC : MultisetCore).
       rewrite (@singleton_mult_in b b); auto with sets.
       rewrite (@singleton_mult_notin b a); eauto with sets.
       rewrite (@singleton_mult_notin b c); eauto with sets.
-      rewrite (@singleton_mult_notin b d); eauto with sets.
+      rewrite (@singleton_mult_notin b d); [|eauto with sets].
       lia.
       setoid_replace c with d; eauto with sets.
       apply meq_multeq; trivial.