diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index e36c89377..ddd5175da 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -36,7 +36,7 @@ type value = (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = { lfun : (identifier * value) list; - lmatch : (int * constr) list; + lmatch : Pattern.patvar_map; debug : debug_info } (* Gives the identifier corresponding to an Identifier [tactic_arg] *) @@ -70,7 +70,7 @@ val add_tacdef : type glob_sign = { ltacvars : identifier list * identifier list; ltacrecvars : (identifier * Nametab.ltac_constant) list; - metavars : int list; + metavars : Rawterm.patvar list; gsigma : Evd.evar_map; genv : Environ.env } @@ -99,7 +99,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Tacred.red_expr (* Interprets tactic expressions *) -val interp_tac_gen : (identifier * value) list -> (int * constr) list -> +val interp_tac_gen : (identifier * value) list -> Pattern.patvar_map -> debug_info -> raw_tactic_expr -> tactic (* Initial call for interpretation *) |