diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f66e5f7083..dec5e811ca 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -80,14 +80,12 @@ let nf_evar_info evc info = | Evar_empty -> Evar_empty | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } -let nf_evars evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm +let nf_evar_map evm = + Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm -let nf_evars_undefined evm = +let nf_evar_map_undefined evm = Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm -let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd -let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd - (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) |