Merge remote-tracking branch 'refs/remotes/origin/master'

fblanqui · Sep 16, 2022 · 4ebc8c5 · 4ebc8c5
2 parents 16f4999 + 1476c05
commit 4ebc8c5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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.