diff options
| author | Arnaud Spiwack | 2014-07-31 16:08:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | 2925c97c852efd66656edebedba543c7c8335b73 (patch) | |
| tree | befa69018bc1e698b5cc73b616cf44c704ecd9d9 /parsing | |
| parent | a7a3f6510643b4fa4bc3299c5111c44b4887873d (diff) | |
New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.
Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.
In other words t;[t1…tn] is [> t;[>t1…tn].. ].
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index dd7687f430..2d9cd3cd41 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -50,16 +50,22 @@ GEXTEND Gram | -> ([TacId []], None) ] ] ; + tactic_then_locality: (* [true] for the local variant [TacThens] and [false] + for [TacExtend] *) + [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] + ; tactic_expr: [ "5" RIGHTA [ te = binder_tactic -> te ] | "4" LEFTA [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) - | ta0 = tactic_expr; ";"; "["; (first,tail) = tactic_then_gen; "]" -> - match tail with - | Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) - | None -> TacThens (ta0,first) ] + | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> + match l , tail with + | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) + | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) + | false , None -> TacThen (ta0,TacDispatch first) + | true , None -> TacThens (ta0,first) ] | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) @@ -107,6 +113,11 @@ GEXTEND Gram TacArg(!@loc,TacCall (!@loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a + | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> + begin match tail with + | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) + | None -> TacDispatch tf + end | a = tactic_atom -> TacArg (!@loc,a) ] ] ; (* binder_tactic: level 5 of tactic_expr *) |