diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
| commit | b33c18ba8edc25c7f4b0be62db4e845dc8693a2f (patch) | |
| tree | 4953c33fc33986555e3b9b5a6f3a84df585bd32f /parsing | |
| parent | 2556a4bcfe9bbad8b3fe555997bb272102fec1dd (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b1ba16b5c..849f67fe6 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) |