diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /pretyping/patternops.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
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 |