diff options
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 |