diff options
| author | herbelin | 2003-05-21 22:38:38 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-21 22:38:38 +0000 |
| commit | 4da48b01f420d8eccf6dcb2fea11bb4d9f8d8a86 (patch) | |
| tree | 611c3f9b178632a5b610d2031dcc1609d5c58419 /tactics/tacinterp.mli | |
| parent | cb601622d7478ca2d61a4c186d992d532f141ace (diff) | |
Suppression définitive de lmatch et or_metanum dans tacinterp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ddd5175da4..9d8a7e57c4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -36,7 +36,6 @@ type value = (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = { lfun : (identifier * value) list; - lmatch : Pattern.patvar_map; debug : debug_info } (* Gives the identifier corresponding to an Identifier [tactic_arg] *) @@ -70,7 +69,6 @@ val add_tacdef : type glob_sign = { ltacvars : identifier list * identifier list; ltacrecvars : (identifier * Nametab.ltac_constant) list; - metavars : Rawterm.patvar list; gsigma : Evd.evar_map; genv : Environ.env } @@ -99,7 +97,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 -> Pattern.patvar_map -> +val interp_tac_gen : (identifier * value) list -> debug_info -> raw_tactic_expr -> tactic (* Initial call for interpretation *) |