diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3c1c470053..248d5d0a0e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -256,7 +256,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) + (* FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) let c = Evarutil.nf_evar sigma c in pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) with Not_found (* List.index failed *) -> @@ -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 |