diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 29 |
1 files changed, 18 insertions, 11 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 7bc3be87a4..eee2cb700c 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -601,19 +601,19 @@ let is_defined d e = EvMap.mem e d.defn_evars let is_undefined d e = EvMap.mem e d.undf_evars -let existential_value d (n, args) = - let info = find d n in - match evar_body info with - | Evar_defined c -> - instantiate_evar_array info c args - | Evar_empty -> - raise NotInstantiatedEvar +let existential_opt_value d (n, args) = + match EvMap.find_opt n d.defn_evars with + | None -> None + | Some info -> + match evar_body info with + | Evar_defined c -> Some (instantiate_evar_array info c args) + | Evar_empty -> None (* impossible but w/e *) -let existential_value0 = existential_value +let existential_value d ev = match existential_opt_value d ev with + | None -> raise NotInstantiatedEvar + | Some v -> v -let existential_opt_value d ev = - try Some (existential_value d ev) - with NotInstantiatedEvar -> None +let existential_value0 = existential_value let existential_opt_value0 = existential_opt_value @@ -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 |