From a92b0e3abb476743f6f12ce828a0d82eb3c98e98 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Sep 2016 17:31:51 +0200 Subject: Move type_uconstr to Tacinterp. --- pretyping/pretyping.ml | 21 --------------------- pretyping/pretyping.mli | 5 ----- 2 files changed, 26 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 156e61ab6..7362b57fe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1203,27 +1203,6 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = true; - use_hook = None; - fail_evar = true; - expand_evars = true } - -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - begin fun env sigma -> - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; - } in - understand_ltac flags env sigma vars expected_type term - end - let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c475bcf7e..aa25e3604 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -84,11 +84,6 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context -val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open - (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) -- cgit v1.2.3