From 411a0c9b05a73d6081f47b0f0f7aa2c859393b76 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 9102960f95..78dd9c3a47 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1192,7 +1192,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