From a43562b661115bebb9353db6ec3b2f6f8dd603ef Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 13 Apr 2016 07:29:51 +0200
Subject: Fixing extra space in printing abbreviations (SyntaxDefinition).

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index bcd38253f..1bd053d9d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -997,7 +997,7 @@ module Make
           return (
             hov 2
               (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
-                 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
+                 prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
                  pr_syntax_modifiers
                  (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
           )
-- 
cgit v1.2.3