diff options
| author | ppedrot | 2013-11-10 04:02:18 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-10 04:02:18 +0000 |
| commit | 6544bd19001a18aea49c30e94a09649f2dcc61e4 (patch) | |
| tree | d8abecbdac9cf8671e0a2d8167e6327d47e8ac83 /intf | |
| parent | 36e41e7581c86214a9f0f97436eb96a75b640834 (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.
This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 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..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 = |