Merge PR #946: Functional pretyping interface

4 files changed, 22 insertions, 3 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f3f2f27e9e..b847aadf21 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac =
     fail_evar = false;
     expand_evars = true
   } in
-  let c = Pretyping.type_uconstr ~flags ist c in
+  let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let replace_in_clause_maybe_by ist c1 c2 cl tac =
@@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c =
     let flags =
       { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
-    let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
+    let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
     let update = begin fun sigma ->
       c env sigma
     end in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 301943a509..5baa0d5c1d 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -48,7 +48,7 @@ let eval_uconstrs ist cs =
     expand_evars = true
   } in
   let map c env sigma = c env sigma in
-  List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
+  List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
 let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d3e625e73a..51eed2f4ec 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function
       :: read_match_rule lfun ist env sigma tl
   | [] -> []
 
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+  ?(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 warn_deprecated_info =
   CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
          (fun () ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 73e4f3d6ab..c1ab2b4c49 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -54,6 +54,11 @@ val set_debug : debug_info -> unit
 (** Gives the state of debug *)
 val get_debug : unit -> debug_info
 
+val type_uconstr :
+  ?flags:Pretyping.inference_flags ->
+  ?expected_type:Pretyping.typing_constraint ->
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+
 (** Adds an interpretation function for extra generic arguments *)
 
 val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t