diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 375ed10d0..9342b4cc7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -279,9 +279,11 @@ let lift_pattern k = liftn_pattern k 1 let rec subst_pattern subst pat = match pat with | PRef ref -> - let ref',t = subst_global subst ref in - if ref' == ref then pat else - pattern_of_constr (Global.env()) Evd.empty t + let ref',t = subst_global subst ref in + if ref' == ref then pat else + let env = Global.env () in + let evd = Evd.from_env env in + pattern_of_constr env evd t | PVar _ | PEvar _ | PRel _ -> pat |