6 files changed, 6 insertions, 62 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 85fb0c73c9..70e5ab38bc 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -48,7 +48,6 @@ let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
  } in
@@ -343,7 +342,6 @@ open Vars
 let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
-  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
@@ -571,44 +569,6 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
     { add_transitivity_lemma false t }
 END
 
-{
-
-let cache_implicit_tactic (_,tac) = match tac with
-  | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
-  | None -> Pfedit.clear_implicit_tactic ()
-
-let subst_implicit_tactic (subst,tac) =
-  Option.map (Tacsubst.subst_tactic subst) tac
-
-let inImplicitTactic : glob_tactic_expr option -> obj =
-  declare_object {(default_object "IMPLICIT-TACTIC") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o);
-       cache_function = cache_implicit_tactic;
-       subst_function = subst_implicit_tactic;
-       classify_function = (fun o -> Dispose)}
-
-let warn_deprecated_implicit_tactic =
-  CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated"
-    (fun () -> strbrk "Implicit tactics are deprecated")
-
-let declare_implicit_tactic tac =
-  let () = warn_deprecated_implicit_tactic () in
-  Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac)))
-
-let clear_implicit_tactic () =
-  let () = warn_deprecated_implicit_tactic () in
-  Lib.add_anonymous_leaf (inImplicitTactic None)
-
-}
-
-VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac }
-| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () }
-END
-
-
-
-
 (**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 5af393a3e5..7be8f67616 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -55,7 +55,6 @@ let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 0f88734caf..1b212334ce 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -700,7 +700,7 @@ type ('b, 'c) argument_interp =
   (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
-  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_parsing : 'a Vernacextend.argument_rule;
   arg_tag : 'c Val.tag option;
   arg_intern : ('a, 'b) argument_intern;
   arg_subst : 'b argument_subst;
@@ -751,10 +751,10 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
   in
   let () = register_interp0 wit (interp_fun name arg tag) in
   let entry = match arg.arg_parsing with
-  | Vernacentries.Arg_alias e ->
+  | Vernacextend.Arg_alias e ->
     let () = Pcoq.register_grammar wit e in
     e
-  | Vernacentries.Arg_rules rules ->
+  | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
     let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
     e
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index c93d6251e0..79f9e093fb 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -128,7 +128,7 @@ type ('b, 'c) argument_interp =
   (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
-  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_parsing : 'a Vernacextend.argument_rule;
   arg_tag : 'c Geninterp.Val.tag option;
   arg_intern : ('a, 'b) argument_intern;
   arg_subst : 'b argument_subst;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2a046a3e65..5bfb0f79fb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -543,7 +543,6 @@ let interp_gen kind ist pattern_mode flags env sigma c =
 let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
@@ -558,21 +557,18 @@ let interp_type = interp_constr_gen IsType
 let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = None;
   fail_evar = false;
   expand_evars = false }
 
@@ -987,7 +983,7 @@ let rec read_match_rule lfun ist env sigma = function
   | [] -> []
 
 (* Fully evaluate an untyped constr *)
-let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+let type_uconstr ?(flags = (constr_flags ()))
   ?(expected_type = WithoutTypeConstraint) ist c =
   begin fun env sigma ->
   let { closure; term } = c in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4626378db6..9173e23b89 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -88,20 +88,9 @@ let subst_reference subst =
 (*CSC: subst_global_reference is used "only" for RefArgType, that propagates
   to the syntactic non-terminals "global", used in commands such as
   Print. It is also used for non-evaluable references. *)
-open Pp
-open Printer
 
 let subst_global_reference subst =
- let subst_global ref =
-  let ref',t' = subst_global subst ref in
-   if not (is_global ref' t') then
-    (let sigma, env = Pfedit.get_current_context () in
-     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
-          str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++
-          pr_global ref'));
-   ref'
- in
-  subst_or_var (subst_located subst_global)
+  subst_or_var (subst_located (subst_global_reference subst))
 
 let subst_evaluable subst =
   let subst_eval_ref = subst_evaluable_reference subst in