diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ac06bb39f3..a4c211de28 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1205,14 +1205,19 @@ module Make ++ str "||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), lorelse - | TacFail (n,l) -> + | TacFail (g,n,l) -> let arg = match n with | ArgArg 0 -> mt () | _ -> pr_arg (pr_or_var int) n in + let name = + match g with + | TacGlobal -> keyword "gfail" + | TacLocal -> keyword "fail" + in hov 1 ( - keyword "fail" ++ arg + name ++ arg ++ prlist (pr_arg (pr_message_token pr.pr_name)) l), latom | TacFirst tl -> |