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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- tactics/tacintern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/tacintern.ml') diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c0e18c1f2..b5731e3bd 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) -> -- cgit v1.2.3