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/constrexpr.mli | |
| 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/constrexpr.mli')
0 files changed, 0 insertions, 0 deletions