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. --- grammar/q_coqast.ml4 | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'grammar') 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.TacLocal -> <:expr> + 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) -- cgit v1.2.3