3 files changed, 36 insertions, 6 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dbbdbfa396..38600695dc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -52,8 +52,11 @@ let () =
 
 (* Rewriting orientation *)
 
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+  Mltop.declare_cache_obj
+    (fun () -> Metasyntax.add_token_obj "<-";
+               Metasyntax.add_token_obj "->")
+    "ltac_plugin"
 
 let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
@@ -196,9 +199,9 @@ let pr_gen_place pr_id = function
     ConclLocation () -> Pp.mt ()
   | HypLocation (id,InHyp) -> str "in " ++ pr_id id
   | HypLocation (id,InHypTypeOnly) ->
-      str "in (Type of " ++ pr_id id ++ str ")"
+      str "in (type of " ++ pr_id id ++ str ")"
   | HypLocation (id,InHypValueOnly) ->
-      str "in (Value of " ++ pr_id id ++ str ")"
+      str "in (value of " ++ pr_id id ++ str ")"
 
 let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id)
 let pr_place _ _ _ = pr_gen_place Id.print
@@ -217,6 +220,14 @@ let interp_place ist gl p =
 
 let subst_place subst pl = pl
 
+let warn_deprecated_instantiate_syntax =
+  CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated"
+         (fun (v,v',id) ->
+           let s = Id.to_string id in
+           Pp.strbrk
+             ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".")
+         )
+
 ARGUMENT EXTEND hloc
     PRINTED BY pr_place
     INTERPRETED BY interp_place
@@ -231,8 +242,14 @@ ARGUMENT EXTEND hloc
 | [ "in" ident(id) ] ->
     [ HypLocation ((CAst.make id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+    [ warn_deprecated_instantiate_syntax ("Type","type",id);
+      HypLocation ((CAst.make id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
+    [ warn_deprecated_instantiate_syntax ("Value","value",id);
+      HypLocation ((CAst.make id),InHypValueOnly) ]
+| [ "in" "(" "type" "of" ident(id) ")" ] ->
+    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+| [ "in" "(" "value" "of" ident(id) ")" ] ->
     [ HypLocation ((CAst.make id),InHypValueOnly) ]
 
  END
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
new file mode 100644
index 0000000000..5611f5ba16
--- /dev/null
+++ b/plugins/ltac/plugin_base.dune
@@ -0,0 +1,13 @@
+(library
+ (name ltac_plugin)
+ (public_name coq.plugins.ltac)
+ (synopsis "Coq's LTAC tactic language")
+ (modules :standard \ tauto)
+ (libraries coq.stm))
+
+(library
+ (name tauto_plugin)
+ (public_name coq.plugins.tauto)
+ (synopsis "Coq's tauto tactic")
+ (modules tauto)
+ (libraries coq.plugins.ltac))
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 0bb9ccb1d8..1f2c722b34 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -144,7 +144,7 @@ let add ~deprecation kn b t =
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
-  let (path, _, _) = KerName.repr path in
+  let path = KerName.modpath path in
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab