diff options
| author | Pierre-Marie Pédrot | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /intf | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 8e5b51b873..b9c41ae03e 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -162,9 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis - (* For ML extensions *) - | TacExtend of Loc.t * ml_tactic_name * 'lev generic_argument list - (* For syntax extensions *) | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list @@ -247,6 +244,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = ('p,('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr) match_rule list | TacFun of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast | TacArg of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg located + (* For ML extensions *) + | TacML of Loc.t * ml_tactic_name * 'l generic_argument list and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast = Id.t option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr |