diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 31c326df6a..f0433d3387 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes -let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes +let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes + +let const_univ_entry = univ_entry let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl @@ -1376,6 +1377,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 |