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.

2 files changed, 5 insertions, 51 deletions

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 *)