diff options
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 |