diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index b5da1b1cb6a3867e62c4506e8a9c14f748247a54..ace17583c1935e4853012ae6af8aacf0ce60334a 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.