diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-31 16:08:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-01 19:18:58 +0200 |
| commit | 2925c97c852efd66656edebedba543c7c8335b73 (patch) | |
| tree | befa69018bc1e698b5cc73b616cf44c704ecd9d9 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d31908114..22ec1b445 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -197,6 +197,12 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = | TacThen of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr + | TacDispatch of + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list + | TacExtendTac of + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr array * + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr array | TacThens of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list |