diff options
| author | Arnaud Spiwack | 2014-12-23 13:06:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-23 13:40:05 +0100 |
| commit | 2fce10d6e0b65f10ac2cd06bf34310b7fce62738 (patch) | |
| tree | 40223f1b8bdc41b9240289e5de2a5e712120345f /grammar | |
| parent | f1699f6dbfa6254041da9ef9d576da05b02ba865 (diff) | |
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.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 8 |
1 files changed, 6 insertions, 2 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) |