diff options
| author | ppedrot | 2013-11-09 02:48:07 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-09 02:48:07 +0000 |
| commit | 485ab2c54051b3c9127477956002956971d41e3b (patch) | |
| tree | 2d32ac92804101a7aaf96c10e32158ccddc0558e /intf | |
| parent | 84388f06b9385b8c194718635ac593083449c4dd (diff) | |
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
Instead of putting the body directly in the AST, we register it in a table.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -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..8f11fdbdac 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 * string * (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 = |