diff options
| author | Arnaud Spiwack | 2014-12-23 13:06:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-23 13:40:05 +0100 |
| commit | 2fce10d6e0b65f10ac2cd06bf34310b7fce62738 (patch) | |
| tree | 40223f1b8bdc41b9240289e5de2a5e712120345f /printing/pptactic.ml | |
| parent | f1699f6dbfa6254041da9ef9d576da05b02ba865 (diff) | |
A global [gfail] tactic which works like [fail] except that it fails even if there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
Diffstat (limited to 'printing/pptactic.ml')
| -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 -> |