diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 0ddf58b74a..87af636b44 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -178,8 +178,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacExtend of Loc.t * string * 'lev generic_argument list (* For syntax extensions *) - | TacAlias of Loc.t * string * - (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr) + | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list (** Possible arguments of a tactic definition *) @@ -250,14 +249,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast = (** Globalized tactics *) -and g_trm = glob_constr_and_expr -and g_pat = glob_constr_and_expr * constr_pattern -and g_cst = evaluable_global_reference and_short_name or_var -and g_ind = inductive or_var -and g_ref = ltac_constant located or_var -and g_nam = Id.t located +type g_trm = glob_constr_and_expr +type g_pat = glob_constr_and_expr * constr_pattern +type g_cst = evaluable_global_reference and_short_name or_var +type g_ind = inductive or_var +type g_ref = ltac_constant located or_var +type g_nam = Id.t located -and glob_tactic_expr = +type glob_tactic_expr = (g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr type glob_atomic_tactic_expr = |