diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6ac857d5c8..dab5c79873 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -71,7 +71,10 @@ let nf_env_evar sigma env = let nf_evar_info evc info = { info with evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps} + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; + evar_body = match info.evar_body with + | Evar_empty -> Evar_empty + | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty |