From 080c5fd2a6cbf390172e086b594b0bd649aa118b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 24 Apr 2018 14:07:39 +0200 Subject: Implement to_constr with nf_evars_and_universes_opt_subst --- engine/evd.ml | 32 ++++++++------------------------ 1 file changed, 8 insertions(+), 24 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 6dcec2760..af22de5cd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1290,30 +1290,14 @@ module MiniEConstr = struct let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = - let rec to_constr c = match Constr.kind c with - | Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr c - | None -> - if abort_on_undefined_evars then - anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") - else - Constr.map (fun c -> to_constr c) c - end - | Sort (Sorts.Type u) -> - let u' = normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> Constr.map (fun c -> to_constr c) c - in to_constr c + let evar_value = + if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev + else fun ev -> + match safe_evar_value sigma ev with + | Some _ as v -> v + | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + in + Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c let of_named_decl d = d let unsafe_to_named_decl d = d -- cgit v1.2.3