aboutsummaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f55ced8090..3305acb779 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -906,8 +906,8 @@ let rec pr_tac inherited tac =
pr_tac (lorelse,E) t2),
lorelse
| TacFail (n,l) ->
- str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
- prlist (pr_arg (pr_message_token pr_ident)) l, latom
+ hov 1 (str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+ prlist (pr_arg (pr_message_token pr_ident)) l), latom
| TacFirst tl ->
str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacSolve tl ->