diff options
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 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) |