diff options
| author | Hugo Herbelin | 2015-10-11 14:36:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-11 15:21:33 +0200 |
| commit | e9995f6e9f9523d4738d9ee494703b6f96bf995d (patch) | |
| tree | ce5297379247c6af9e6c16ba45b5b7e479b96d3c /tactics | |
| parent | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (diff) | |
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
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 |