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.
---
 intf/tacexpr.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index c4e91d32ee..1e5d1e61d4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -25,6 +25,9 @@ type lazy_flag =
   | Select  (* returns all successes of the first matching branch *)
   | Once    (* returns the first success in a maching branch
                (not necessarily the first) *)
+type global_flag = (* [gfail] or [fail] *)
+  | TacGlobal
+  | TacLocal
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
@@ -271,7 +274,7 @@ and 'a gen_tactic_expr =
   | TacAbstract of
       'a gen_tactic_expr * Id.t option
   | TacId of 'n message_token list
-  | TacFail of int or_var * 'n message_token list
+  | TacFail of global_flag * int or_var * 'n message_token list
   | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
       (Id.t located * 'a gen_tactic_arg) list *
-- 
cgit v1.2.3