Merge PR #1114: Generic handling of nameable objects for plugins

22 files changed, 242 insertions, 104 deletions

diff --git a/API/API.ml b/API/API.ml
index 46ad36d36d..bf99d0febd 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -212,7 +212,7 @@ module Pputils = Pputils
 module Ppconstr = Ppconstr
 module Printer = Printer
 (* module Printmod *)
-(* module Prettyp *)
+module Prettyp = Prettyp
 module Ppvernac = Ppvernac
 
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index 3ed326ff0e..3bd047043a 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 :
@@ -4975,6 +5005,21 @@ sig
   val pr_transparent_state : Names.transparent_state -> Pp.t
 end
 
+module Prettyp :
+sig
+  type 'a locatable_info = {
+    locate : Libnames.qualid -> 'a option;
+    locate_all : Libnames.qualid -> 'a list;
+    shortest_qualid : 'a -> Libnames.qualid;
+    name : 'a -> Pp.t;
+    print : 'a -> Pp.t;
+    about : 'a -> Pp.t;
+  }
+
+  val register_locatable : string -> 'a locatable_info -> unit
+  val print_located_other : string -> Libnames.reference -> Pp.t
+end
+
 (************************************************************************)
 (* End of modules from printing/                                        *)
 (************************************************************************)
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 03e8ea43d1..4a471d4a2b 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -91,7 +91,7 @@ type locatable =
   | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
-  | LocateTactic of reference
+  | LocateOther of string * reference
   | LocateFile of string
 
 type showable =
diff --git a/library/nametab.ml b/library/nametab.ml
index 68fdbb4f38..0ec4a37cdb 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 025a63b1ce..3a380637c2 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/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 819d236cd3..3e0b85b54a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1020,8 +1020,7 @@ GEXTEND Gram
       | IDENT "Term"; qid = smart_global -> LocateTerm qid
       | IDENT "File"; f = ne_string -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary qid
-      | IDENT "Module"; qid = global -> LocateModule qid
-      | IDENT "Ltac"; qid = global -> LocateTactic qid ] ]
+      | IDENT "Module"; qid = global -> LocateModule qid ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue (Some n)
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 86c983bdd9..d639dd0e1c 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -482,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
   [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
 
+VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
+| [ "Locate" "Ltac" reference(r) ] ->
+  [ Tacentries.print_located_tactic r ]
+END
+
 let pr_ltac_ref = Libnames.pr_reference
 
 let pr_tacdef_body tacdef_body =
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 12b4c81fc4..3972b7aac3 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 d8bd166208..d588c888c4 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 c79d5b389f..d9da954fe6 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 a8d518fbd8..bcd5b388a1 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
@@ -506,6 +506,31 @@ let print_ltacs () =
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
 
+let locatable_ltac = "Ltac"
+
+let () =
+  let open Prettyp in
+  let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
+  let locate_all = Tacenv.locate_extended_all_tactic in
+  let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
+  let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+  let print kn =
+    let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
+    Tacintern.print_ltac qid
+  in
+  let about = name in
+  register_locatable locatable_ltac {
+    locate;
+    locate_all;
+    shortest_qualid;
+    name;
+    print;
+    about;
+  }
+
+let print_located_tactic qid =
+  Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+
 (** Grammar *)
 
 let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index aa8f4efe65..ab2c6b3073 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -62,3 +62,6 @@ val create_ltac_quotation : string ->
 
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
+
+val print_located_tactic : Libnames.reference -> unit
+(** Display the absolute name of a tactic. *)
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 13b44f0e2c..8c59a36fa6 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 958109e5a7..4ecc978fea 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 64da097deb..2c36faeff4 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 fc6ee6aab6..99d7684d36 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 cf5fdf3184..d37c676e38 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 1e1a986daa..7b591feada 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/ppvernac.ml b/printing/ppvernac.ml
index 10dd42ea91..a1cdfdbaa2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1156,7 +1156,7 @@ open Decl_kinds
           | LocateFile f -> keyword "File" ++ spc() ++ qs f
           | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
           | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
-          | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
+          | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
         in
         return (keyword "Locate" ++ spc() ++ pr_locate loc)
       | VernacRegister (id, RegisterInline) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 09859157c3..2077526db4 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -304,14 +304,33 @@ let print_inductive_argument_scopes =
 (*********************)
 (* "Locate" commands *)
 
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  locate_all : qualid -> 'a list;
+  shortest_qualid : 'a -> qualid;
+  name : 'a -> Pp.t;
+  print : 'a -> Pp.t;
+  about : 'a -> Pp.t;
+}
+
+type locatable = Locatable : 'a locatable_info -> locatable
+
 type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
   | Syntactic of kernel_name
   | ModuleType of module_path
-  | Tactic of Nametab.ltac_constant
+  | Other : 'a * 'a locatable_info -> logical_name
   | Undefined of qualid
 
+(** Generic table for objects that are accessible through a name. *)
+let locatable_map : locatable String.Map.t ref = ref String.Map.empty
+
+let register_locatable name f =
+  locatable_map := String.Map.add name (Locatable f) !locatable_map
+
+exception ObjFound of logical_name
+
 let locate_any_name ref =
   let (loc,qid) = qualid_of_reference ref in
   try Term (Nametab.locate qid)
@@ -321,7 +340,13 @@ let locate_any_name ref =
   try Dir (Nametab.locate_dir qid)
   with Not_found ->
   try ModuleType (Nametab.locate_modtype qid)
-  with Not_found -> Undefined qid
+  with Not_found ->
+    let iter _ (Locatable info) = match info.locate qid with
+    | None -> ()
+    | Some ans -> raise (ObjFound (Other (ans, info)))
+    in
+    try String.Map.iter iter !locatable_map; Undefined qid
+    with ObjFound obj -> obj
 
 let pr_located_qualid = function
   | Term ref ->
@@ -344,8 +369,7 @@ 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)
+  | Other (obj, info) -> info.name obj
   | Undefined qid ->
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -383,10 +407,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
@@ -408,13 +428,30 @@ let locate_modtype qid =
   in
   modtypes @ List.map_filter map all
 
+let locate_other s qid =
+  let Locatable info = String.Map.find s !locatable_map in
+  let ans = info.locate_all qid in
+  let map obj = (Other (obj, info), info.shortest_qualid obj) in
+  List.map map ans
+
+type locatable_kind =
+| LocTerm
+| LocModule
+| LocOther of string
+| LocAny
+
 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
+  let located = match flags with
+  | LocTerm -> locate_term qid
+  | LocModule -> locate_modtype qid @ locate_module qid
+  | LocOther s -> locate_other s qid
+  | LocAny ->
+    locate_term qid @
+    locate_modtype qid @
+    locate_module qid @
+    String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map []
+  in
   match located with
     | [] ->
 	let (dir,id) = repr_qualid qid in
@@ -432,10 +469,10 @@ let print_located_qualid name flags ref =
 	   else mt ()) ++
           display_alias o)) l
 
-let print_located_term ref = print_located_qualid "term" [`TERM] ref
-let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref
-let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref
-let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref
+let print_located_term ref = print_located_qualid "term" LocTerm ref
+let print_located_other s ref = print_located_qualid s (LocOther s) ref
+let print_located_module ref = print_located_qualid "module" LocModule ref
+let print_located_qualid ref = print_located_qualid "object" LocAny ref
 
 (******************************************)
 (**** Printing declarations and judgments *)
@@ -765,7 +802,7 @@ 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 *)
+  | Other (obj, info) -> info.print obj
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
@@ -822,8 +859,9 @@ 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)
+  | Other (obj, info) -> hov 0 (info.about obj)
 
 let print_about = function
   | ByNotation (loc,(ntn,sc)) ->
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index f4277b6c50..dbd1011593 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -50,12 +50,34 @@ val print_all_instances : unit -> Pp.t
 
 val inspect : int -> Pp.t
 
-(** Locate *)
+(** {5 Locate} *)
+
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  (** Locate the most precise object with the provided name if any. *)
+  locate_all : qualid -> 'a list;
+  (** Locate all objects whose name is a suffix of the provided name *)
+  shortest_qualid : 'a -> qualid;
+  (** Return the shortest name in the current context *)
+  name : 'a -> Pp.t;
+  (** Data as printed by the Locate command *)
+  print : 'a -> Pp.t;
+  (** Data as printed by the Print command *)
+  about : 'a -> Pp.t;
+  (** Data as printed by the About command *)
+}
+(** Generic data structure representing locatable objects. *)
+
+val register_locatable : string -> 'a locatable_info -> unit
+(** Define a new type of locatable objects that can be reached via the
+    corresponding generic vernacular commands. The string should be a unique
+    name describing the kind of objects considered and that is added as a
+    grammar command prefix for vernacular commands Locate. *)
 
 val print_located_qualid : reference -> Pp.t
 val print_located_term : reference -> Pp.t
-val print_located_tactic : reference -> Pp.t
 val print_located_module : reference -> Pp.t
+val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
   print_inductive           : mutual_inductive -> Pp.t;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 83296cf58f..203d913db8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> msg_notice (print_located_module qid)
-  | LocateTactic qid -> msg_notice (print_located_tactic qid)
+  | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
   | LocateFile f -> msg_notice (locate_file f)
 
 let vernac_register id r =