From f6f3b9c6dee84958ceafb1806670fcad593508ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 23:55:43 +0200
Subject: [PATCH] Fix prettty printing of multiset literals.

---
 theories/base.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index be247b96..a0507871 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -938,10 +938,11 @@ Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
 Instance: Params (@singletonMS) 3 := {}.
-Notation "{[+ x +]}" := (singletonMS x) (at level 1) : stdpp_scope.
+Notation "{[+ x +]}" := (singletonMS x)
+  (at level 1, format "{[+  x  +]}") : stdpp_scope.
 Notation "{[+ x ; y ; .. ; z +]}" :=
   (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
-  (at level 1) : stdpp_scope.
+  (at level 1, format "{[+  x ;  y ;  .. ;  z  +]}") : stdpp_scope.
 
 Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
-- 
GitLab