From 00d7fbc1e12947d9494ce2c4b79f462a7b2bac08 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Oct 2018 19:38:41 +0200
Subject: [PATCH] =?UTF-8?q?Proper=20pretty=20printing=20of=20new=20`|=3D{E?=
 =?UTF-8?q?,E'}=E2=96=B7=3D>^n`=20notation.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/notation.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 4a8dd7f51..c64497696 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -88,7 +88,8 @@ Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
 Reserved Notation "|={ E1 , E2 }â–·=>^ n Q"
-  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200).
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "|={ E1 , E2 }â–·=>^ n  Q").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
-- 
GitLab