Move type_uconstr to Tacinterp.

2 files changed, 0 insertions, 26 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 156e61ab65..7362b57fe4 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 c475bcf7e8..aa25e36048 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. *)