diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a7573f5343..7476dc0a7d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -426,12 +426,14 @@ let whd_betadeltaiota_nolet env sigma x = (* Replacing defined evars for error messages *) let rec whd_evar sigma c = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + | Evar (ev,args) + when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> whd_evar sigma (Evd.existential_value sigma (ev,args)) + | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar sigma = - local_strong (whd_evar sigma) +let nf_evar evd = + local_strong (whd_evar evd) (* lazy reduction functions. The infos must be created for each term *) let clos_norm_flags flgs env sigma t = |