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 /tactics/tacintern.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 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c0e18c1f2..b5731e3bd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -611,8 +611,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) - | TacFail (n,l) -> - ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l) + | TacFail (g,n,l) -> + ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l) | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac) | TacAbstract (tac,s) -> |