From 7c8f942767ebaba7dd4f7b86487b3145bf3a652a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 18:42:29 +0100
Subject: [PATCH] Fix pretty printing of big op notations.

---
 algebra/upred_big_op.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index d7f75b7ec..25d744197 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -18,12 +18,12 @@ Definition uPred_big_sepM {M} `{FinMapToList K A MA}
     (m : MA) (P : K → A → uPred M) : uPred M :=
   uPred_big_sep (curry P <$> map_to_list m).
 Notation "'Π★{map' m } P" := (uPred_big_sepM m P)
-  (at level 20, m at level 10, format "Π★{map m }  P") : uPred_scope.
+  (at level 20, m at level 10, format "Π★{map  m }  P") : uPred_scope.
 
 Definition uPred_big_sepS {M} `{Elements A C}
   (X : C) (P : A → uPred M) : uPred M := uPred_big_sep (P <$> elements X).
 Notation "'Π★{set' X } P" := (uPred_big_sepS X P)
-  (at level 20, X at level 10, format "Π★{set X }  P") : uPred_scope.
+  (at level 20, X at level 10, format "Π★{set  X }  P") : uPred_scope.
 
 (** * Always stability for lists *)
 Class AlwaysStableL {M} (Ps : list (uPred M)) :=
-- 
GitLab