diff options
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 c4e91d32ee..1e5d1e61d4 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 * |