[api] Remove deprecated aliases from `Names`.

2 files changed, 4 insertions, 359 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 1f2666a95..54f089e60 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -760,55 +760,8 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
 (*******************************************************************)
 (** Compatibility layers *)
 
-(** Backward compatibility for [Id] *)
-
-type identifier = Id.t
-
-let id_eq = Id.equal
-let id_ord = Id.compare
-let string_of_id = Id.to_string
-let id_of_string = Id.of_string
-
-module Idset = Id.Set
-module Idmap = Id.Map
-module Idpred = Id.Pred
-
-(** Compatibility layer for [Name] *)
-
-let name_eq = Name.equal
-
-(** Compatibility layer for [DirPath] *)
-
-type dir_path = DirPath.t
-let dir_path_ord = DirPath.compare
-let dir_path_eq = DirPath.equal
-let make_dirpath = DirPath.make
-let repr_dirpath = DirPath.repr
-let empty_dirpath = DirPath.empty
-let is_empty_dirpath = DirPath.is_empty
-let string_of_dirpath = DirPath.to_string
-let initial_dir = DirPath.initial
-
-(** Compatibility layer for [MBId] *)
-
 type mod_bound_id = MBId.t
-let mod_bound_id_ord = MBId.compare
-let mod_bound_id_eq = MBId.equal
-let make_mbid = MBId.make
-let repr_mbid = MBId.repr
-let debug_string_of_mbid = MBId.debug_to_string
-let string_of_mbid = MBId.to_string
-let id_of_mbid = MBId.to_id
-
-(** Compatibility layer for [Label] *)
-
-type label = Id.t
-let mk_label = Label.make
-let string_of_label = Label.to_string
-let pr_label = Label.print
-let id_of_label = Label.to_id
-let label_of_id = Label.of_id
-let eq_label = Label.equal
+let eq_constant_key = Constant.UserOrd.equal
 
 (** Compatibility layer for [ModPath] *)
 
@@ -816,32 +769,13 @@ type module_path = ModPath.t =
   | MPfile of DirPath.t
   | MPbound of MBId.t
   | MPdot of module_path * Label.t
-let check_bound_mp = ModPath.is_bound
-let string_of_mp = ModPath.to_string
-let mp_ord = ModPath.compare
-let mp_eq = ModPath.equal
-let initial_path = ModPath.initial
-
-(** Compatibility layer for [KerName] *)
-
-type kernel_name = KerName.t
-let make_kn = KerName.make
-let repr_kn = KerName.repr
-let modpath = KerName.modpath
-let label = KerName.label
-let string_of_kn = KerName.to_string
-let pr_kn = KerName.print
-let kn_ord = KerName.compare
 
 (** Compatibility layer for [Constant] *)
 
-type constant = Constant.t
-
+module Projection =
+struct
+  type t = Constant.t * bool
 
-module Projection = 
-struct 
-  type t = constant * bool
-    
   let make c b = (c, b)
 
   let constant = fst
@@ -918,40 +852,3 @@ let eq_egr e1 e2 = match e1, e2 with
     EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
   | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
   | _, _ -> false
-
-let constant_of_kn = Constant.make1
-let constant_of_kn_equiv = Constant.make
-let make_con = Constant.make3
-let repr_con = Constant.repr3
-let canonical_con = Constant.canonical
-let user_con = Constant.user
-let con_label = Constant.label
-let con_modpath = Constant.modpath
-let eq_constant = Constant.equal
-let eq_constant_key = Constant.UserOrd.equal
-let con_ord = Constant.CanOrd.compare
-let con_user_ord = Constant.UserOrd.compare
-let string_of_con = Constant.to_string
-let pr_con = Constant.print
-let debug_string_of_con = Constant.debug_to_string
-let debug_pr_con = Constant.debug_print
-let con_with_label = Constant.change_label
-
-(** Compatibility layer for [MutInd] *)
-
-type mutual_inductive = MutInd.t
-let mind_of_kn = MutInd.make1
-let mind_of_kn_equiv = MutInd.make
-let make_mind = MutInd.make3
-let canonical_mind = MutInd.canonical
-let user_mind = MutInd.user
-let repr_mind = MutInd.repr3
-let mind_label = MutInd.label
-let mind_modpath = MutInd.modpath
-let eq_mind = MutInd.equal
-let mind_ord = MutInd.CanOrd.compare
-let mind_user_ord = MutInd.UserOrd.compare
-let string_of_mind = MutInd.to_string
-let pr_mind = MutInd.print
-let debug_string_of_mind = MutInd.debug_to_string
-let debug_pr_mind = MutInd.debug_print
diff --git a/kernel/names.mli b/kernel/names.mli
index fdaa228fd..f988b559a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -538,116 +538,8 @@ val eq_ind_chk : inductive -> inductive -> bool
 
 (** {6 Deprecated functions. For backward compatibility.} *)
 
-(** {5 Identifiers} *)
-
-type identifier = Id.t
-[@@ocaml.deprecated "Alias for [Id.t]"]
-
-val string_of_id : Id.t -> string
-[@@ocaml.deprecated "Same as [Id.to_string]."]
-
-val id_of_string : string -> Id.t
-[@@ocaml.deprecated "Same as [Id.of_string]."]
-
-val id_ord : Id.t -> Id.t -> int
-[@@ocaml.deprecated "Same as [Id.compare]."]
-
-val id_eq : Id.t -> Id.t -> bool
-[@@ocaml.deprecated "Same as [Id.equal]."]
-
-module Idset  : Set.S with type elt = Id.t and type t = Id.Set.t
-[@@ocaml.deprecated "Same as [Id.Set]."]
-
-module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t
-[@@ocaml.deprecated "Same as [Id.Pred]."]
-
-module Idmap : module type of Id.Map
-[@@ocaml.deprecated "Same as [Id.Map]."]
-
-(** {5 Directory paths} *)
-
-type dir_path = DirPath.t
-[@@ocaml.deprecated "Alias for [DirPath.t]."]
-
-val dir_path_ord : DirPath.t -> DirPath.t -> int
-[@@ocaml.deprecated "Same as [DirPath.compare]."]
-
-val dir_path_eq : DirPath.t -> DirPath.t -> bool
-[@@ocaml.deprecated "Same as [DirPath.equal]."]
-
-val make_dirpath : module_ident list -> DirPath.t
-[@@ocaml.deprecated "Same as [DirPath.make]."]
-
-val repr_dirpath : DirPath.t -> module_ident list
-[@@ocaml.deprecated "Same as [DirPath.repr]."]
-
-val empty_dirpath : DirPath.t
-[@@ocaml.deprecated "Same as [DirPath.empty]."]
-
-val is_empty_dirpath : DirPath.t -> bool
-[@@ocaml.deprecated "Same as [DirPath.is_empty]."]
-
-val string_of_dirpath : DirPath.t -> string
-[@@ocaml.deprecated "Same as [DirPath.to_string]."]
-
-val initial_dir : DirPath.t
-[@@ocaml.deprecated "Same as [DirPath.initial]."]
-
-(** {5 Labels} *)
-
-type label = Label.t
-[@@ocaml.deprecated "Same as [Label.t]."]
-(** Alias type *)
-
-val mk_label : string -> Label.t
-[@@ocaml.deprecated "Same as [Label.make]."]
-
-val string_of_label : Label.t -> string
-[@@ocaml.deprecated "Same as [Label.to_string]."]
-
-val pr_label : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Label.print]."]
-
-val label_of_id : Id.t -> Label.t
-[@@ocaml.deprecated "Same as [Label.of_id]."]
-
-val id_of_label : Label.t -> Id.t
-[@@ocaml.deprecated "Same as [Label.to_id]."]
-
-val eq_label : Label.t -> Label.t -> bool
-[@@ocaml.deprecated "Same as [Label.equal]."]
-
-(** {5 Unique bound module names} *)
-
 type mod_bound_id = MBId.t
 [@@ocaml.deprecated "Same as [MBId.t]."]
-
-val mod_bound_id_ord : MBId.t -> MBId.t -> int
-[@@ocaml.deprecated "Same as [MBId.compare]."]
-
-val mod_bound_id_eq : MBId.t -> MBId.t -> bool
-[@@ocaml.deprecated "Same as [MBId.equal]."]
-
-val make_mbid : DirPath.t -> Id.t -> MBId.t
-[@@ocaml.deprecated "Same as [MBId.make]."]
-
-val repr_mbid : MBId.t -> int * Id.t * DirPath.t
-[@@ocaml.deprecated "Same as [MBId.repr]."]
-
-val id_of_mbid : MBId.t -> Id.t
-[@@ocaml.deprecated "Same as [MBId.to_id]."]
-
-val string_of_mbid : MBId.t -> string
-[@@ocaml.deprecated "Same as [MBId.to_string]."]
-
-val debug_string_of_mbid : MBId.t -> string
-[@@ocaml.deprecated "Same as [MBId.debug_to_string]."]
-
-(** {5 Names} *)
-
-val name_eq : Name.t -> Name.t -> bool
-[@@ocaml.deprecated "Same as [Name.equal]."]
-
 (** {5 Module paths} *)
 
 type module_path = ModPath.t =
@@ -656,52 +548,6 @@ type module_path = ModPath.t =
   | MPdot of ModPath.t * Label.t
 [@@ocaml.deprecated "Alias type"]
 
-val mp_ord : ModPath.t -> ModPath.t -> int
-[@@ocaml.deprecated "Same as [ModPath.compare]."]
-
-val mp_eq : ModPath.t -> ModPath.t -> bool
-[@@ocaml.deprecated "Same as [ModPath.equal]."]
-
-val check_bound_mp : ModPath.t -> bool
-[@@ocaml.deprecated "Same as [ModPath.is_bound]."]
-
-val string_of_mp : ModPath.t -> string
-[@@ocaml.deprecated "Same as [ModPath.to_string]."]
-
-val initial_path : ModPath.t
-[@@ocaml.deprecated "Same as [ModPath.initial]."]
-
-(** {5 Kernel names} *)
-
-type kernel_name = KerName.t
-[@@ocaml.deprecated "Alias type"]
-
-val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t
-[@@ocaml.deprecated "Same as [KerName.make]."]
-
-val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t
-[@@ocaml.deprecated "Same as [KerName.repr]."]
-
-val modpath : KerName.t -> ModPath.t
-[@@ocaml.deprecated "Same as [KerName.modpath]."]
-
-val label : KerName.t -> Label.t
-[@@ocaml.deprecated "Same as [KerName.label]."]
-
-val string_of_kn : KerName.t -> string
-[@@ocaml.deprecated "Same as [KerName.to_string]."]
-
-val pr_kn : KerName.t -> Pp.t
-[@@ocaml.deprecated "Same as [KerName.print]."]
-
-val kn_ord : KerName.t -> KerName.t -> int
-[@@ocaml.deprecated "Same as [KerName.compare]."]
-
-(** {5 Constant names} *)
-
-type constant = Constant.t
-[@@ocaml.deprecated "Alias type"]
-
 module Projection : sig
   type t
 
@@ -759,101 +605,3 @@ type evaluable_global_reference =
   | EvalConstRef of Constant.t
 
 val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
-
-val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
-[@@ocaml.deprecated "Same as [Constant.make]"]
-
-val constant_of_kn : KerName.t -> Constant.t
-[@@ocaml.deprecated "Same as [Constant.make1]"]
-
-val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t
-[@@ocaml.deprecated "Same as [Constant.make3]"]
-
-val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t
-[@@ocaml.deprecated "Same as [Constant.repr3]"]
-
-val user_con : Constant.t -> KerName.t
-[@@ocaml.deprecated "Same as [Constant.user]"]
-
-val canonical_con : Constant.t -> KerName.t
-[@@ocaml.deprecated "Same as [Constant.canonical]"]
-
-val con_modpath : Constant.t -> ModPath.t
-[@@ocaml.deprecated "Same as [Constant.modpath]"]
-
-val con_label : Constant.t -> Label.t
-[@@ocaml.deprecated "Same as [Constant.label]"]
-
-val eq_constant : Constant.t -> Constant.t -> bool
-[@@ocaml.deprecated "Same as [Constant.equal]"]
-
-val con_ord : Constant.t -> Constant.t -> int
-[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"]
-
-val con_user_ord : Constant.t -> Constant.t -> int
-[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"]
-
-val con_with_label : Constant.t -> Label.t -> Constant.t
-[@@ocaml.deprecated "Same as [Constant.change_label]"]
-
-val string_of_con : Constant.t -> string
-[@@ocaml.deprecated "Same as [Constant.to_string]"]
-
-val pr_con : Constant.t -> Pp.t
-[@@ocaml.deprecated "Same as [Constant.print]"]
-
-val debug_pr_con : Constant.t -> Pp.t
-[@@ocaml.deprecated "Same as [Constant.debug_print]"]
-
-val debug_string_of_con : Constant.t -> string
-[@@ocaml.deprecated "Same as [Constant.debug_to_string]"]
-
-(** {5 Mutual Inductive names} *)
-
-type mutual_inductive = MutInd.t
-[@@ocaml.deprecated "Alias type"]
-
-val mind_of_kn : KerName.t -> MutInd.t
-[@@ocaml.deprecated "Same as [MutInd.make1]"]
-
-val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t
-[@@ocaml.deprecated "Same as [MutInd.make]"]
-
-val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t
-[@@ocaml.deprecated "Same as [MutInd.make3]"]
-
-val user_mind : MutInd.t -> KerName.t
-[@@ocaml.deprecated "Same as [MutInd.user]"]
-
-val canonical_mind : MutInd.t -> KerName.t
-[@@ocaml.deprecated "Same as [MutInd.canonical]"]
-
-val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t
-[@@ocaml.deprecated "Same as [MutInd.repr3]"]
-
-val eq_mind : MutInd.t -> MutInd.t -> bool
-[@@ocaml.deprecated "Same as [MutInd.equal]"]
-
-val mind_ord : MutInd.t -> MutInd.t -> int
-[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"]
-
-val mind_user_ord : MutInd.t -> MutInd.t -> int
-[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"]
-
-val mind_label : MutInd.t -> Label.t
-[@@ocaml.deprecated "Same as [MutInd.label]"]
-
-val mind_modpath : MutInd.t -> ModPath.t
-[@@ocaml.deprecated "Same as [MutInd.modpath]"]
-
-val string_of_mind : MutInd.t -> string
-[@@ocaml.deprecated "Same as [MutInd.to_string]"]
-
-val pr_mind : MutInd.t -> Pp.t
-[@@ocaml.deprecated "Same as [MutInd.print]"]
-
-val debug_pr_mind : MutInd.t -> Pp.t
-[@@ocaml.deprecated "Same as [MutInd.debug_print]"]
-
-val debug_string_of_mind : MutInd.t -> string
-[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"]