From a2664de27eabbba7fc357305679112aef99e1f74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 16:39:55 +0200
Subject: Removing automatic printing of leading space in auto_using and
 hintbases so that it does not put extra space when auto is defined as a
 TACTIC EXTEND.

---
 printing/pptactic.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7dae97acf2..7d7ebd1416 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -675,15 +675,13 @@ module Make
             str " ]")
 
   let pr_hintbases = function
-    | None -> spc () ++ keyword "with" ++ str" *"
+    | None -> keyword "with" ++ str" *"
     | Some [] -> mt ()
-    | Some l ->
-      spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+    | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
 
   let pr_auto_using prc = function
     | [] -> mt ()
-    | l -> spc () ++
-      hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+    | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
   let pr_then () = str ";"
 
-- 
cgit v1.2.3