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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a1b99de87b..d2c8c45033 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -102,8 +102,8 @@ GEXTEND Gram | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l | IDENT "idtac"; l = LIST0 message_token -> TacId l - | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; - l = LIST0 message_token -> TacFail (n,l) + | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; + l = LIST0 message_token -> TacFail (g,n,l) | st = simple_tactic -> st | IDENT "constr"; ":"; c = Constr.constr -> TacArg(!@loc,ConstrMayEval(ConstrTerm c)) @@ -119,6 +119,9 @@ GEXTEND Gram end | a = tactic_atom -> TacArg (!@loc,a) ] ] ; + failkw: + [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] + ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: [ RIGHTA |