From 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 10:17:26 +0200
Subject: Fixing extra space in printing bullets.

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e5f3d58644..7ba1f44392 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1196,7 +1196,7 @@ module Make
             | Dash n -> str (String.make n '-')
             | Star n -> str (String.make n '*')
             | Plus n -> str (String.make n '+')
-          end ++ spc())
+          end)
         | VernacSubproof None ->
           return (str "{")
         | VernacSubproof (Some i) ->
-- 
cgit v1.2.3