diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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 |