diff options
author | 2016-03-20 20:41:17 +0100 | |
---|---|---|
committer | 2016-03-20 21:03:32 +0100 | |
commit | c3de822e711fa3f10817432b7023fc2f88c0aeeb (patch) | |
tree | 5c9f9713cb09aa63c2351a994cd9b8b62d8a8715 /pretyping/evarutil.mli | |
parent | e98d7276f52c4b67bf05a80a6b44f334966f82fd (diff) |
Making Evarutil independent from Reductionops.
Diffstat (limited to 'pretyping/evarutil.mli')
-rw-r--r-- | pretyping/evarutil.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a4f852765..ffff2c5dd 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -78,6 +78,8 @@ val new_evar_instance : val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list +val safe_evar_value : evar_map -> existential -> constr option + (** {6 Evars/Metas switching...} *) val non_instantiated : evar_map -> evar_info Evar.Map.t @@ -96,9 +98,6 @@ val has_undefined_evars : evar_map -> constr -> bool val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool -(** [check_evars env initial_sigma extended_sigma c] fails if some - new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit (** [gather_dependent_evars evm seeds] classifies the evars in [evm] as dependent_evars and goals (these may overlap). A goal is an @@ -134,6 +133,7 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains uninstantiated; [nf_evar] leaves uninstantiated evars as is *) +val whd_evar : evar_map -> constr -> constr val nf_evar : evar_map -> constr -> constr val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment val jl_nf_evar : @@ -151,9 +151,6 @@ val nf_evar_info : evar_map -> evar_info -> evar_info val nf_evar_map : evar_map -> evar_map val nf_evar_map_undefined : evar_map -> evar_map -val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment -val jv_nf_betaiotaevar : - evar_map -> unsafe_judgment array -> unsafe_judgment array (** Presenting terms without solved evars *) val nf_evars_universes : evar_map -> constr -> constr |