diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8875d1d936..39015d89a9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -973,9 +973,9 @@ let e_contextually byhead (occs,c) f env sigma t = else t with ConstrMatching.PatternMatchingFailure -> - Evarsolve.map_constr_with_binders_left_to_right + map_constr_with_binders_left_to_right (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) - traverse envc sigma t + traverse envc t in let t' = traverse (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; |