diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/nametab.ml | 47 | ||||
| -rw-r--r-- | library/nametab.mli | 9 |
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 *) |