From b776e361c2091e18cb7b41cc87cf555cd93ea289 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 17:49:17 +0100
Subject: [PATCH] fix print spacing of telescopes

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

diff --git a/theories/telescopes.v b/theories/telescopes.v
index 6b7f5213..1f8c8795 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -125,7 +125,7 @@ Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
 (** Notation *)
 Notation "'[tele' x .. z ]" :=
   (TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))
-  (x binder, z binder, format "[tele  '[hv' x .. z ']' ]").
+  (x binder, z binder, format "[tele  '[hv' x  ..  z ']' ]").
 Notation "'[tele' ]" := (TeleO)
   (format "[tele ]").
 
-- 
GitLab