Moving the Ltac-specific part of the nametab to the Ltac plugin.

For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.

14 files changed, 109 insertions, 87 deletions

diff --git a/API/API.mli b/API/API.mli
index 3ed326ff0..e2cb70583 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1795,6 +1795,7 @@ sig
   val pr_path : full_path -> Pp.t
   val make_path : Names.DirPath.t -> Names.Id.t -> full_path
   val eq_full_path : full_path -> full_path -> bool
+  val repr_path : full_path -> Names.DirPath.t * Names.Id.t
   val dirpath : full_path -> Names.DirPath.t
   val path_of_string : string -> full_path
 
@@ -1935,24 +1936,19 @@ module Nametab :
 sig
   exception GlobalizationError of Libnames.qualid
 
-  type ltac_constant = Names.KerName.t
-
   val global : Libnames.reference -> Globnames.global_reference
   val global_of_path : Libnames.full_path -> Globnames.global_reference
   val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid
   val path_of_global : Globnames.global_reference -> Libnames.full_path
   val locate_extended : Libnames.qualid -> Globnames.extended_global_reference
   val full_name_module : Libnames.qualid -> Names.DirPath.t
-  val locate_tactic : Libnames.qualid -> Names.KerName.t
   val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t
-  val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid
   val basename_of_global : Globnames.global_reference -> Names.Id.t
 
   type visibility =
     | Until of int
     | Exactly of int
 
-  val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit
   val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a
   val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid
   val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
@@ -1960,6 +1956,40 @@ sig
   val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t
   val locate : Libnames.qualid -> Globnames.global_reference
   val locate_constant : Libnames.qualid -> Names.Constant.t
+
+  (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
+
+  module type UserName = sig
+    type t
+    val equal : t -> t -> bool
+    val to_string : t -> string
+    val repr : t ->  Names.Id.t * Names.Id.t list
+  end
+
+  module type EqualityType =
+  sig
+    type t
+    val equal : t -> t -> bool
+  end
+
+  module type NAMETREE = sig
+    type elt
+    type t
+    type user_name
+
+    val empty : t
+    val push : visibility -> user_name -> elt -> t -> t
+    val locate : Libnames.qualid -> t -> elt
+    val find : user_name -> t -> elt
+    val exists : user_name -> t -> bool
+    val user_name : Libnames.qualid -> t -> user_name
+    val shortest_qualid : Names.Id.Set.t -> user_name -> t -> Libnames.qualid
+    val find_prefixes : Libnames.qualid -> t -> elt list
+  end
+
+  module Make (U : UserName) (E : EqualityType) :
+    NAMETREE with type user_name = U.t and type elt = E.t
+
 end
 
 module Global :
diff --git a/library/nametab.ml b/library/nametab.ml
index 68fdbb4f3..0ec4a37cd 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -19,10 +19,6 @@ exception GlobalizationError of qualid
 let error_global_not_found ?loc q =
   Loc.raise ?loc (GlobalizationError q)
 
-(* Kinds of global names *)
-
-type ltac_constant = kernel_name
-
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
      is loaded inside a module
@@ -274,19 +270,14 @@ struct
 end
 
 module ExtRefEqual = ExtRefOrdered
-module KnEqual = Names.KerName
 module MPEqual = Names.ModPath
 
 module ExtRefTab = Make(FullPath)(ExtRefEqual)
-module KnTab = Make(FullPath)(KnEqual)
 module MPTab = Make(FullPath)(MPEqual)
 
 type ccitab = ExtRefTab.t
 let the_ccitab = ref (ExtRefTab.empty : ccitab)
 
-type kntab = KnTab.t
-let the_tactictab = ref (KnTab.empty : kntab)
-
 type mptab = MPTab.t
 let the_modtypetab = ref (MPTab.empty : mptab)
 
@@ -327,10 +318,6 @@ let the_modrevtab = ref (MPmap.empty : mprevtab)
 type mptrevtab = full_path MPmap.t
 let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
 
-type knrevtab = full_path KNmap.t
-let the_tacticrevtab = ref (KNmap.empty : knrevtab)
-
-
 (* Push functions *********************************************************)
 
 (* This is for permanent constructions (never discharged -- but with
@@ -368,13 +355,6 @@ let push_modtype vis sp kn =
   the_modtypetab := MPTab.push vis sp kn !the_modtypetab;
   the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
-(* This is for tactic definition names *)
-
-let push_tactic vis sp kn =
-  the_tactictab := KnTab.push vis sp kn !the_tactictab;
-  the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
-
-
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 let push_dir vis dir dir_ref =
   the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
@@ -402,8 +382,6 @@ let locate_syndef qid = match locate_extended qid with
 let locate_modtype qid = MPTab.locate qid !the_modtypetab
 let full_name_modtype qid = MPTab.user_name qid !the_modtypetab
 
-let locate_tactic qid = KnTab.locate qid !the_tactictab
-
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
 let locate_module qid =
@@ -428,8 +406,6 @@ let locate_all qid =
 
 let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
-let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab
-
 let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
 
 let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
@@ -471,8 +447,6 @@ let exists_module = exists_dir
 
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
-let exists_tactic kn = KnTab.exists kn !the_tactictab
-
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
@@ -492,9 +466,6 @@ let path_of_syndef kn =
 let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
 
-let path_of_tactic kn =
-  KNmap.find kn !the_tacticrevtab
-
 let path_of_modtype mp =
   MPmap.find mp !the_modtyperevtab
 
@@ -519,10 +490,6 @@ let shortest_qualid_of_modtype kn =
   let sp = MPmap.find kn !the_modtyperevtab in
     MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_tactic kn =
-  let sp = KNmap.find kn !the_tacticrevtab in
-    KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
-
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
@@ -541,28 +508,24 @@ let global_inductive r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * mptab * kntab
-    * globrevtab * mprevtab * mptrevtab * knrevtab
+type frozen = ccitab * dirtab * mptab
+    * globrevtab * mprevtab * mptrevtab
 
 let freeze _ : frozen =
   !the_ccitab,
   !the_dirtab,
   !the_modtypetab,
-  !the_tactictab,
   !the_globrevtab,
   !the_modrevtab,
-  !the_modtyperevtab,
-  !the_tacticrevtab
+  !the_modtyperevtab
 
-let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) =
+let unfreeze (ccit,dirt,mtyt,globr,modr,mtyr) =
   the_ccitab := ccit;
   the_dirtab := dirt;
   the_modtypetab := mtyt;
-  the_tactictab := tact;
   the_globrevtab := globr;
   the_modrevtab := modr;
-  the_modtyperevtab := mtyr;
-  the_tacticrevtab := tacr
+  the_modtyperevtab := mtyr
 
 let _ =
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index 025a63b1c..3a380637c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -78,10 +78,6 @@ val push_modtype : visibility -> full_path -> module_path -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-type ltac_constant = kernel_name
-val push_tactic : visibility -> full_path -> ltac_constant -> unit
-
-
 (** {6 The following functions perform globalization of qualified names } *)
 
 (** These functions globalize a (partially) qualified name or fail with
@@ -95,7 +91,6 @@ val locate_modtype : qualid -> module_path
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> module_path
 val locate_section : qualid -> DirPath.t
-val locate_tactic : qualid -> ltac_constant
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -109,7 +104,6 @@ val global_inductive : reference -> inductive
 
 val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
-val locate_extended_all_tactic : qualid -> ltac_constant list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> module_path list
 
@@ -125,7 +119,6 @@ val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
 val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
 val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
-val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *)
 
 (** {6 These functions locate qualids into full user names } *)
 
@@ -144,7 +137,6 @@ val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
 val dirpath_of_module : module_path -> DirPath.t
 val path_of_modtype : module_path -> full_path
-val path_of_tactic : ltac_constant -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -166,7 +158,6 @@ val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
 val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
 val shortest_qualid_of_module : module_path -> qualid
-val shortest_qualid_of_tactic : ltac_constant -> qualid
 
 (** Deprecated synonyms *)
 
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 12b4c81fc..3972b7aac 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,9 +1,9 @@
 Tacarg
+Tacsubst
+Tacenv
 Pptactic
 Pltac
 Taccoerce
-Tacsubst
-Tacenv
 Tactic_debug
 Tacintern
 Tacentries
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d8bd16620..d588c888c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -336,7 +336,7 @@ type 'a extra_genarg_printer =
   let pr_ltac_constant kn =
     if !Flags.in_debugger then KerName.print kn
     else try
-           pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+           pr_qualid (Tacenv.shortest_qualid_of_tactic kn)
       with Not_found -> (* local tactic not accessible anymore *)
         str "<" ++ KerName.print kn ++ str ">"
 
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index c79d5b389..d9da954fe 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t
 val pr_alias : (Val.t -> Pp.t) ->
   int -> Names.KerName.t -> Val.t list -> Pp.t
 
-val pr_ltac_constant : Nametab.ltac_constant -> Pp.t
+val pr_ltac_constant : ltac_constant -> Pp.t
 
 val pr_raw_tactic : raw_tactic_expr -> Pp.t
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a8d518fbd..8573da19f 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) =
 
 type tacdef_kind =
   | NewTac of Id.t
-  | UpdateTac of Nametab.ltac_constant
+  | UpdateTac of Tacexpr.ltac_constant
 
 let is_defined_tac kn =
   try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
@@ -441,7 +441,7 @@ let register_ltac local tacl =
     | Tacexpr.TacticRedefinition (ident, body) ->
         let loc = loc_of_reference ident in
         let kn =
-          try Nametab.locate_tactic (snd (qualid_of_reference ident))
+          try Tacenv.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
             CErrors.user_err ?loc 
                        (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
@@ -464,7 +464,7 @@ let register_ltac local tacl =
   let defs () =
     (** Register locally the tactic to handle recursivity. This function affects
         the whole environment, so that we transactify it afterwards. *)
-    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+    let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
     let () = List.iter iter_rec recvars in
     List.map map rfun
   in
@@ -475,7 +475,7 @@ let register_ltac local tacl =
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
   | UpdateTac kn ->
     Tacenv.redefine_ltac local kn tac;
-    let name = Nametab.shortest_qualid_of_tactic kn in
+    let name = Tacenv.shortest_qualid_of_tactic kn in
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
   List.iter iter defs
@@ -488,7 +488,7 @@ let print_ltacs () =
   let entries = List.sort sort entries in
   let map (kn, entry) =
     let qid =
-      try Some (Nametab.shortest_qualid_of_tactic kn)
+      try Some (Tacenv.shortest_qualid_of_tactic kn)
       with Not_found -> None
     in
     match qid with
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 13b44f0e2..8c59a36fa 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -11,6 +11,42 @@ open Pp
 open Names
 open Tacexpr
 
+(** Nametab for tactics *)
+
+(** TODO: Share me somewhere *)
+module FullPath =
+struct
+  open Libnames
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+      id, (DirPath.repr dir)
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+
+let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty)
+
+let push_tactic vis sp kn =
+  let (tab, revtab) = !tactic_tab in
+  let tab = KnTab.push vis sp kn tab in
+  let revtab = KNmap.add kn sp revtab in
+  tactic_tab := (tab, revtab)
+
+let locate_tactic qid = KnTab.locate qid (fst !tactic_tab)
+
+let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab)
+
+let exists_tactic kn = KnTab.exists kn (fst !tactic_tab)
+
+let path_of_tactic kn = KNmap.find kn (snd !tactic_tab)
+
+let shortest_qualid_of_tactic kn =
+  let sp = KNmap.find kn (snd !tactic_tab) in
+  KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab)
+
 (** Tactic notations (TacAlias) *)
 
 type alias = KerName.t
@@ -103,19 +139,19 @@ let replace kn path t =
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
-  let () = if not local then Nametab.push_tactic (Until i) sp kn in
+  let () = if not local then push_tactic (Until i) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
 let open_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
-  let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
+  let () = if not local then push_tactic (Exactly i) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
 let cache_md ((sp, kn), (local, id ,b, t)) = match id with
 | None ->
-  let () = Nametab.push_tactic (Until 1) sp kn in
+  let () = push_tactic (Until 1) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
@@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) =
 
 let classify_md (local, _, _, _ as o) = Substitute o
 
-let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 958109e5a..4ecc978fe 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -7,11 +7,21 @@
 (************************************************************************)
 
 open Names
+open Libnames
 open Tacexpr
 open Geninterp
 
 (** This module centralizes the various ways of registering tactics. *)
 
+(** {5 Tactic naming} *)
+
+val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit
+val locate_tactic : qualid -> ltac_constant
+val locate_extended_all_tactic : qualid -> ltac_constant list
+val exists_tactic : full_path -> bool
+val path_of_tactic : ltac_constant -> full_path
+val shortest_qualid_of_tactic : ltac_constant -> qualid
+
 (** {5 Tactic notations} *)
 
 type alias = KerName.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 64da097de..2c36faeff 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -10,13 +10,14 @@ open Loc
 open Names
 open Constrexpr
 open Libnames
-open Nametab
 open Genredexpr
 open Genarg
 open Pattern
 open Misctypes
 open Locus
 
+type ltac_constant = KerName.t
+
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fc6ee6aab..99d7684d3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function
 
 let intern_isolated_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[]))
+  TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
 
 let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
@@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r =
 
 let intern_applied_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  ArgArg (loc,locate_tactic qid)
+  ArgArg (loc,Tacenv.locate_tactic qid)
 
 let intern_applied_tactic_reference ist r =
   (* An ltac reference *)
@@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n
 
 let print_ltac id =
  try
-  let kn = Nametab.locate_tactic id in
+  let kn = Tacenv.locate_tactic id in
   let entries = Tacenv.ltac_entries () in
   let tac = KNmap.find kn entries in
   let filter mp =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cf5fdf318..d37c676e3 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -814,8 +814,8 @@ let ssr_n_tac seed n gl =
   let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in
   let fail msg = CErrors.user_err (Pp.str msg) in
   let tacname = 
-    try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
-    with Not_found -> try Nametab.locate_tactic (ssrqid name)
+    try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
+    with Not_found -> try Tacenv.locate_tactic (ssrqid name)
     with Not_found ->
       if n = -1 then fail "The ssreflect library was not loaded"
       else fail ("The tactic "^name^" was not found") in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 1e1a986da..7b591fead 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1554,8 +1554,8 @@ END
 let ssrautoprop gl =
   try 
     let tacname = 
-      try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
-      with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in
+      try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
+      with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
     Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
   with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 09859157c..b2e7fe447 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -309,7 +309,6 @@ type logical_name =
   | Dir of global_dir_reference
   | Syntactic of kernel_name
   | ModuleType of module_path
-  | Tactic of Nametab.ltac_constant
   | Undefined of qualid
 
 let locate_any_name ref =
@@ -344,8 +343,6 @@ let pr_located_qualid = function
       str s ++ spc () ++ pr_dirpath dir
   | ModuleType mp ->
       str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
-  | Tactic kn ->
-      str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn)
   | Undefined qid ->
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -383,10 +380,6 @@ let locate_term qid =
   in
   List.map expand (Nametab.locate_extended_all qid)
 
-let locate_tactic qid =
-  let all = Nametab.locate_extended_all_tactic qid in
-  List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all
-
 let locate_module qid =
   let all = Nametab.locate_extended_all_dir qid in
   let map dir = match dir with
@@ -411,7 +404,6 @@ let locate_modtype qid =
 let print_located_qualid name flags ref =
   let (loc,qid) = qualid_of_reference ref in
   let located = [] in
-  let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in
   let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in
   let located = if List.mem `MODULE flags then locate_module qid @ located else located in
   let located = if List.mem `TERM flags then locate_term qid @ located else located in
@@ -765,7 +757,6 @@ let print_any_name = function
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
-  | Tactic kn -> mt () (** TODO *)
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
@@ -822,7 +813,7 @@ let print_about_any ?loc k =
       v 0 (
       print_syntactic_def kn ++ fnl () ++
       hov 0 (str "Expands to: " ++ pr_located_qualid k))
-  | Dir _ | ModuleType _ | Tactic _ | Undefined _ ->
+  | Dir _ | ModuleType _ | Undefined _ ->
       hov 0 (pr_located_qualid k)
 
 let print_about = function