9 files changed, 17 insertions, 81 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5463893ad0..ea8dcf57dd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -10,7 +10,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b830342..4e7c8b754f 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,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,Notation_term.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a4f090ed..ff697e3c75 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -66,7 +66,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_gram.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 17011f2067..cb7183638e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Constr
 open Genarg
 open Stdarg
 open Tacarg
@@ -284,78 +285,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
 END
 
 (**********************************************************************)
-(* Hint Resolve                                                       *)
-
-open Term
-open EConstr
-open Vars
-open Coqlib
-
-let project_hint ~poly pri l2r r =
-  let gr = Smartlocate.global_with_alias r in
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma c in
-  let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
-  let sign,ccl = decompose_prod_assum sigma t in
-  let (a,b) = match snd (decompose_app sigma ccl) with
-    | [a;b] -> (a,b)
-    | _ -> assert false in
-  let p =
-    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let sigma, p = Evd.fresh_global env sigma p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
-  let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
-  let id =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let ctx = Evd.const_univ_entry ~poly sigma in
-  let c = EConstr.to_constr sigma c in
-  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
-
-let add_hints_iff ~atts l2r lc n bl =
-  let open Vernacinterp in
-  Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
-    (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
-
-VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
-  [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
-    ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts true lc n bl;
-        st
-      end
-  ]
-| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts true lc n ["core"];
-        st
-      end
-  ]
-END
-
-VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
-  [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
-    ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts false lc n bl;
-        st
-      end
-  ]
-| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts false lc n ["core"];
-        st
-      end
-  ]
-END
-
-(**********************************************************************)
 (* Refine                                                             *)
 
 open EConstr
@@ -594,10 +523,16 @@ let inImplicitTactic : glob_tactic_expr option -> obj =
        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
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 07047d0162..642e521556 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Constr
 open Genarg
 open Stdarg
 open Pcoq.Prim
@@ -169,7 +170,7 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
 END
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3dfe308a5d..b29af6680d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
 open Geninterp
 open Stdarg
 open Libnames
-open Notation_term
+open Notation_gram
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 799a52cc8b..5d2a996183 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,7 +17,7 @@ open Names
 open Misctypes
 open Environ
 open Constrexpr
-open Notation_term
+open Notation_gram
 open Tacexpr
 
 type 'a grammar_tactic_prod_item_expr =
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 val ltop : tolerability
 
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
   'a Genprint.top_printer
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a1d8b087e8..50bf687b1d 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) =
   (bvars,subst_glob_constr subst c,subst_pattern subst p)
 
 let subst_redexp subst =
-  Miscops.map_red_expr_gen
+  Redops.map_red_expr_gen
     (subst_glob_constr subst)
     (subst_evaluable subst)
     (subst_glob_constr_or_pattern subst)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index a51c09ca4f..8eeb8903e7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Hipattern
 open Names