From 0609eec7cf1f05fc4364f43d5503c4165b484b46 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 May 2020 15:18:40 +0200
Subject: [PATCH] Avoid space in pretty printing of session types.

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

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 72a84d9..3bea14a 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -39,7 +39,7 @@ Instance: Params (@lty_app) 1 := {}.
 
 Notation "'TY' A ; S" := (lty_msg_base A S)
   (at level 200, right associativity,
-   format "'TY'  A  ;  S") : lmsg_scope.
+   format "'TY'  A ;  S") : lmsg_scope.
 Notation "∃ X .. Y , M" :=
   (lty_msg_exist (λ X, .. (lty_msg_exist (λ Y, M)) ..)%lmsg) : lmsg_scope.
 Notation "'∃..' X .. Y , M" :=
-- 
GitLab