From 7f9c67249d9ae8792d54459e82627d9bd2cd33c9 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 bullets."

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7ba1f44392..e5f3d58644 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)
+          end ++ spc())
         | VernacSubproof None ->
           return (str "{")
         | VernacSubproof (Some i) ->
-- 
cgit v1.2.3