diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 593e46b05..96d0b592b 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) |