diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:25:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:28:19 +0200 |
| commit | 4b7de15309da63b30f53325383ead7004b1f2c26 (patch) | |
| tree | f49e277bb60a50bd8421ae86093acd23dde66904 /intf | |
| parent | 243ffa4b928486122075762da6ce8da707e07daf (diff) | |
Moving the TacAlias node out of atomic tactics.
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 b9c41ae03..cf8d34d7e 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 syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list - (** Possible arguments of a tactic definition *) and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg = @@ -246,6 +243,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = | 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 + (* For syntax extensions *) + | TacAlias of Loc.t * KerName.t * (Id.t * '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 |