diff options
| author | ppedrot | 2013-11-09 07:08:59 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-09 07:08:59 +0000 |
| commit | 36e41e7581c86214a9f0f97436eb96a75b640834 (patch) | |
| tree | 2c99a4b163e976272c7931d0889611d8c13a15ae /intf | |
| parent | 485ab2c54051b3c9127477956002956971d41e3b (diff) | |
Revert the previous commit. It broke Coq compilation.
Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 8f11fdbdac..0ddf58b74a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -178,7 +178,8 @@ 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 + | TacAlias of Loc.t * string * + (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr) (** Possible arguments of a tactic definition *) @@ -249,14 +250,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast = (** Globalized tactics *) -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 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 glob_tactic_expr = +and glob_tactic_expr = (g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr type glob_atomic_tactic_expr = |