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.
---
 printing/pptactic.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'printing')

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