7 files changed, 2 insertions, 78 deletions
diff --git a/library/global.ml b/library/global.ml
index 55aed1c56e..06e06a8cf2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -157,11 +157,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-let type_of_global_in_context = Typeops.type_of_global_in_context
-
-let universes_of_global gr = 
-  universes_of_global (env ()) gr
-
 let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
diff --git a/library/global.mli b/library/global.mli
index 76ac3f6279..a60de48897 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -131,14 +131,6 @@ val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
 val is_type_in_type : GlobRef.t -> bool
 
-val type_of_global_in_context : Environ.env -> 
-  GlobRef.t -> Constr.types * Univ.AUContext.t
-  [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]
-
-(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : GlobRef.t -> Univ.AUContext.t
-[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
-
 (** {6 Retroknowledge } *)
 
 val register_inline : Constant.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index db2e8bfaed..99dcc43ad1 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -85,15 +85,6 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-module RefOrdered = Names.GlobRef.Ordered
-module RefOrdered_env = Names.GlobRef.Ordered_env
-
-module Refmap = Names.GlobRef.Map
-module Refset = Names.GlobRef.Set
-
-module Refmap_env = Names.GlobRef.Map_env
-module Refset_env = Names.GlobRef.Set_env
-
 (* Extended global references *)
 
 type syndef_name = KerName.t
@@ -134,6 +125,3 @@ end
 type global_reference_or_constr = 
   | IsGlobal of global_reference
   | IsConstr of constr
-
-(* Deprecated *)
-let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index d49ed453f5..14e422b743 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -25,8 +25,6 @@ val isConstRef : GlobRef.t -> bool
 val isIndRef : GlobRef.t -> bool
 val isConstructRef : GlobRef.t -> bool
 
-val eq_gr : GlobRef.t -> GlobRef.t -> bool
-[@@ocaml.deprecated "Use Names.GlobRef.equal"]
 val canonical_gr : GlobRef.t -> GlobRef.t
 
 val destVarRef : GlobRef.t -> variable
@@ -48,22 +46,6 @@ val printable_constr_of_global : GlobRef.t -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> GlobRef.t
 
-module RefOrdered = Names.GlobRef.Ordered
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
-
-module RefOrdered_env = Names.GlobRef.Ordered_env
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
-
-module Refset = Names.GlobRef.Set
-[@@ocaml.deprecated "Use Names.GlobRef.Set"]
-module Refmap = Names.GlobRef.Map
-[@@ocaml.deprecated "Use Names.GlobRef.Map"]
-
-module Refset_env = GlobRef.Set_env
-[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
-module Refmap_env = GlobRef.Map_env
-[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
-
 (** {6 Extended global references } *)
 
 type syndef_name = KerName.t
diff --git a/library/lib.ml b/library/lib.ml
index d4381a6923..a046360822 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -278,7 +278,7 @@ let start_mod is_type export id mp fs =
   let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
-    else Nametab.exists_module dir
+    else Nametab.exists_dir dir
   in
   if exists then
     user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
@@ -569,7 +569,7 @@ let open_section id =
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
-  if Nametab.exists_section obj_dir then
+  if Nametab.exists_dir obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
   add_entry (make_foname id) (OpenedSection (prefix, fs));
diff --git a/library/nametab.ml b/library/nametab.ml
index 95890b2edf..bd0ea5f04f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -43,12 +43,6 @@ module GlobDirRef = struct
 
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-let eq_global_dir_reference = GlobDirRef.equal
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 let error_global_not_found qid =
@@ -516,10 +510,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab
 
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
-let exists_section = exists_dir
-
-let exists_module = exists_dir
-
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
@@ -585,10 +575,3 @@ let global_inductive qid =
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type")
-
-(********************************************************************)
-
-(* Deprecated synonyms *)
-
-let extended_locate = locate_extended
-let absolute_reference = global_of_path
diff --git a/library/nametab.mli b/library/nametab.mli
index fccb8fd918..a4f177aad0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -89,13 +89,6 @@ module GlobDirRef : sig
   val equal : t -> t -> bool
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-val eq_global_dir_reference :
-  GlobDirRef.t -> GlobDirRef.t -> bool
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
@@ -170,10 +163,6 @@ val extended_global_of_path : full_path -> extended_global_reference
 val exists_cci : full_path -> bool
 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_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
@@ -220,11 +209,6 @@ val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
-(** Deprecated synonyms *)
-
-val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
-val absolute_reference : full_path -> GlobRef.t (** = global_of_path *)
-
 (** {5 Generic name handling} *)
 
 (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)