From d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6670aa41ab..396add2646 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1001,7 +1001,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