diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-23 13:06:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-23 13:40:05 +0100 |
| commit | 2fce10d6e0b65f10ac2cd06bf34310b7fce62738 (patch) | |
| tree | 40223f1b8bdc41b9240289e5de2a5e712120345f /intf | |
| 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 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index c4e91d32e..1e5d1e61d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -25,6 +25,9 @@ type lazy_flag = | Select (* returns all successes of the first matching branch *) | Once (* returns the first success in a maching branch (not necessarily the first) *) +type global_flag = (* [gfail] or [fail] *) + | TacGlobal + | TacLocal type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) @@ -271,7 +274,7 @@ and 'a gen_tactic_expr = | TacAbstract of 'a gen_tactic_expr * Id.t option | TacId of 'n message_token list - | TacFail of int or_var * 'n message_token list + | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * (Id.t located * 'a gen_tactic_arg) list * |