diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a3ab250784..248d5d0a0e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -279,10 +279,12 @@ 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 - let env = Global.env () in - let evd = Evd.from_env env in - pattern_of_constr env evd t + if ref' == ref then pat else (match t with + | None -> PRef ref' + | Some t -> + let env = Global.env () in + let evd = Evd.from_env env in + pattern_of_constr env evd t.Univ.univ_abstracted_value) | PVar _ | PEvar _ | PRel _ -> pat |