From 2fce10d6e0b65f10ac2cd06bf34310b7fce62738 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Dec 2014 13:06:35 +0100
Subject: 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.
---
 parsing/g_ltac.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3