diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 7 | ||||
| -rw-r--r-- | tactics/tactic_matching.mli | 4 |
2 files changed, 6 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 593e46b05c..96d0b592b8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1038,11 +1038,12 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt (* Reads a pattern by substituting vars of lfun *) let use_types = false -let eval_pattern lfun ist env sigma (_,pat as c) = +let eval_pattern lfun ist env sigma ((glob,_),pat as c) = + let bound_names = bound_glob_vars glob in if use_types then - pi3 (interp_typed_pattern ist env sigma c) + (bound_names,pi3 (interp_typed_pattern ist env sigma c)) else - instantiate_pattern env sigma lfun pat + (bound_names,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli index abeb47c3b9..d8e6dd0ae3 100644 --- a/tactics/tactic_matching.mli +++ b/tactics/tactic_matching.mli @@ -32,7 +32,7 @@ val match_term : Environ.env -> Evd.evar_map -> Term.constr -> - (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic (** [match_goal env sigma hyps concl rules] matches the goal @@ -45,5 +45,5 @@ val match_goal: Evd.evar_map -> Context.named_context -> Term.constr -> - (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic |