8 files changed, 26 insertions, 7 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 6097951330..89feea8dcf 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -249,7 +249,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b06f35ddc4..00668ddc7d 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -64,7 +64,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
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/pptactic.ml b/plugins/ltac/pptactic.ml
index 140cc33440..cb7d9b9c02 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Geninterp
 open Stdarg
 open Tacarg
 open Libnames
-open Ppextend
+open Notation_term
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0bf9bc7f62..1f6ebaf448 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,7 @@ open Misctypes
 open Environ
 open Constrexpr
 open Tacexpr
-open Ppextend
+open Notation_term
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
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