diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 36b674fe5a..5fc4ff8db3 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -134,6 +134,10 @@ val tj_nf_evar : val nf_evar_info : evar_map -> evar_info -> evar_info val nf_evars : evar_map -> evar_map +val nf_named_context_evar : evar_map -> named_context -> named_context +val nf_rel_context_evar : evar_map -> rel_context -> rel_context +val nf_env_evar : evar_map -> env -> env + (* Same for evar defs *) val nf_isevar : evar_defs -> constr -> constr val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment |