diff options
| author | Maxime Dénès | 2019-01-17 10:51:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-21 10:26:04 +0100 |
| commit | 10a9c492a486fcb884ffeadd1d05ecb0fae90d0f (patch) | |
| tree | 17b373d5d6212482c9971bf2d8aa1dd79b3fdb67 /engine | |
| parent | 05e2222e04323d11429d659b415750cf40e2babd (diff) | |
[EConstr] Expose API to normalize and check if evars are remaining
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.mli | 3 | ||||
| -rw-r--r-- | engine/evd.ml | 7 | ||||
| -rw-r--r-- | engine/evd.mli | 1 |
3 files changed, 11 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6532e08e9d..49cbc4d7e5 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *) +val to_constr_opt : Evd.evar_map -> t -> Constr.t option +(** Same as [to_constr], but returns [None] if some unresolved evars remain *) + val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) diff --git a/engine/evd.ml b/engine/evd.ml index 31c326df6a..eee2cb700c 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1376,6 +1376,13 @@ module MiniEConstr = struct in UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c + let to_constr_opt sigma c = + let evar_value ev = Some (existential_value sigma ev) in + try + Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c) + with NotInstantiatedEvar -> + None + let of_named_decl d = d let unsafe_to_named_decl d = d let of_rel_decl d = d diff --git a/engine/evd.mli b/engine/evd.mli index 7560d68805..de73144895 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -689,6 +689,7 @@ module MiniEConstr : sig val of_constr_array : Constr.t array -> t array val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t + val to_constr_opt : evar_map -> t -> Constr.t option val unsafe_to_constr : t -> Constr.t val unsafe_to_constr_array : t array -> Constr.t array |