From 080f60258407d8cf0f8991f763bafe1b6363ac57 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing extra space in printing abbreviations
 (SyntaxDefinition)."

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 396add2646..6670aa41ab 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_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
+                 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
                  pr_syntax_modifiers
                  (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
           )
-- 
cgit v1.2.3