Moving back some tactics not essentially related to Ltac into the tactics/ folder.

2 files changed, 33 insertions, 0 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a765d30913..8baa668c7b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -58,6 +58,8 @@ type ltac_var_map = {
 }
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -1107,3 +1109,26 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W
 
 let understand_ltac flags env sigma lvar kind c =
   ise_pretype_gen flags env sigma lvar kind c
+
+let constr_flags = {
+  use_typeclasses = true;
+  use_unif_heuristics = 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 =
+  { delayed = 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 = ist.Geninterp.lfun;
+  } in
+  let sigma = Sigma.to_evar_map sigma in
+  let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
+  Sigma.Unsafe.of_pair (c, sigma)
+  end }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 4c4c535d8c..91320f20a5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -55,6 +55,9 @@ type inference_flags = {
   expand_evars : bool
 }
 
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags
@@ -114,6 +117,11 @@ val understand_judgment : env -> evar_map ->
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
+val type_uconstr :
+  ?flags:inference_flags ->
+  ?expected_type:typing_constraint ->
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)