From b33c18ba8edc25c7f4b0be62db4e845dc8693a2f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Nov 2011 08:46:27 +0000
Subject: Fixing beautification of "thm_token" (missing space) + improvements.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14654 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b1ba16b5cf..849f67fe68 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -414,8 +414,8 @@ let pr_grammar_tactic_rule n (_,pil,t) =
 
 let pr_statement head (id,(bl,c,guard)) =
   assert (id<>None);
-  hov 0
-    (head ++ pr_lident (Option.get id) ++ spc() ++
+  hov 1
+    (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
     pr_opt (pr_guard_annot bl) guard ++
     str":" ++ pr_spc_lconstr c)
-- 
cgit v1.2.3