From 03127e9d454385a1e2baf9f6912f077598b25782 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Mar 2019 18:50:15 +0100
Subject: [PATCH] Fix weird thing that should not have worked.

---
 theories/gmultiset.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index b5da1b1c..ace17583 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -215,7 +215,7 @@ Proof.
   by rewrite multiplicity_disj_union, multiplicity_empty.
 Qed.
 Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
-Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed.
+Proof. intros X. by rewrite (comm_L (⊎)), (left_id_L _ _). Qed.
 
 Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎).
 Proof.
-- 
GitLab