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.

7 files changed, 32 insertions, 12 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index c7d126c37d..23c4538b3b 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -62,6 +62,10 @@ let mlexpr_of_by_notation f = function
       let loc = of_coqloc loc in
       <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
 
+let mlexpr_of_global_flag = function
+  | Tacexpr.TacGlobal -> <:expr<Tacexpr.TacGlobal>>
+  | Tacexpr.TacLocal  -> <:expr<Tacexpr.TacLocal>>
+
 let mlexpr_of_intro_pattern_disjunctive = function
   _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO"
 
@@ -468,8 +472,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
   | Tacexpr.TacId l ->
       <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
-  | Tacexpr.TacFail (n,l) ->
-      <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >>
+  | Tacexpr.TacFail (g,n,l) ->
+      <:expr< Tacexpr.TacFail $mlexpr_of_global_flag g$ $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >>
 (*
   | Tacexpr.TacInfo t -> TacInfo (loc,f t)
 
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 *
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
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ac06bb39f3..a4c211de28 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1205,14 +1205,19 @@ module Make
                 ++ str "||" ++ brk (1,1)
                 ++ pr_tac (lorelse,E) t2),
               lorelse
-            | TacFail (n,l) ->
+            | TacFail (g,n,l) ->
               let arg =
                 match n with
                   | ArgArg 0 -> mt ()
                   | _ -> pr_arg (pr_or_var int) n
               in
+              let name =
+                match g with
+                | TacGlobal -> keyword "gfail"
+                | TacLocal -> keyword "fail"
+              in
               hov 1 (
-                keyword "fail" ++ arg
+                name ++ arg
                 ++ prlist (pr_arg (pr_message_token pr.pr_name)) l),
               latom
             | TacFirst tl ->
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index dfb3def564..5351e41698 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -222,7 +222,7 @@ let initial_atomic () =
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
   List.iter iter
       [ "idtac",TacId [];
-        "fail", TacFail(ArgArg 0,[]);
+        "fail", TacFail(TacLocal,ArgArg 0,[]);
         "fresh", TacArg(dloc,TacFreshId [])
       ]
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c0e18c1f28..b5731e3bd5 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -611,8 +611,8 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars,
       TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
-  | TacFail (n,l) ->
-      ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l)
+  | TacFail (g,n,l) ->
+      ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
   | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
   | TacAbstract (tac,s) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 967d7d7b8b..89f6fbc747 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1133,9 +1133,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run msgnl begin fun msgnl ->
         print msgnl <*> log msgnl <*> break
       end
-  | TacFail (n,s) ->
+  | TacFail (g,n,s) ->
       let msg = interp_message ist s in
-      let tac l = Proofview.tclINDEPENDENT (Tacticals.New.tclFAIL (interp_int_or_var ist n) l) in
+      let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in
+      let tac =
+        match g with
+        | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l)
+        | TacGlobal -> tac
+      in
       Ftactic.run msg tac
   | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
   | TacShowHyps tac ->