Merge PR #6065: [api] Deprecate all legacy uses of Names in core.

9 files changed, 24 insertions, 24 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index bd8f3db50..0ead94eff 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -136,31 +136,31 @@ let check_exists sp =
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' =
     match obj.cst_decl with
     | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
-      then constant_of_kn kn
+      then Constant.make1 kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     | Some decl ->
       let () = check_exists sp in
       Global.add_constant dir id decl
   in
-  assert (eq_constant kn' (constant_of_kn kn));
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+  assert (Constant.equal kn' (Constant.make1 kn));
+  Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
   add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind
+  add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharged_hyps kn sechyps =
-  let (_,dir,_) = repr_kn kn in
+  let (_,dir,_) = KerName.repr kn in
   let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev_map (Libnames.make_path dir) args
 
 let discharge_constant ((sp, kn), obj) =
-  let con = constant_of_kn kn in
+  let con = Constant.make1 kn in
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
   let hyps,subst,uctx = section_segment_of_constant con in
@@ -311,9 +311,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists (List.map fst names);
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' = Global.add_mind dir id mie in
-  assert (eq_mind kn' (mind_of_kn kn));
+  assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
   add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
@@ -384,7 +384,7 @@ let declare_projections mind =
 	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
-	  assert(eq_constant kn kn')) kns; true,true
+	  assert(Constant.equal kn kn')) kns; true,true
     | Some None -> true,false
     | None -> false,false
 
diff --git a/interp/declare.mli b/interp/declare.mli
index ccd7d28bb..86d33cfb2 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -52,17 +52,17 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent *)
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
-  constr Univ.in_universe_context_set -> constant
+  constr Univ.in_universe_context_set -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
-  (string -> (inductive * constant) array -> unit) -> unit
+  (string -> (inductive * Constant.t) array -> unit) -> unit
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 561b0078a..13ed65056 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -231,7 +231,7 @@ let add_glob ?loc ref =
     add_glob_gen ?loc sp lib_dp ty
 
 let mp_of_kn kn =
-  let mp,sec,l = Names.repr_kn kn in
+  let mp,sec,l = Names.KerName.repr kn in
     Names.MPdot (mp,l)
 
 let add_glob_kn ?loc kn =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index afcd7a2ed..f3ad50f28 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -23,11 +23,11 @@ val pause : unit -> unit
 val continue : unit -> unit
 
 val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
-val add_glob_kn : ?loc:Loc.t -> Names.kernel_name -> unit
+val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
 val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit
-val dump_moddef : ?loc:Loc.t -> Names.module_path -> string -> unit
-val dump_modref  : ?loc:Loc.t -> Names.module_path -> string -> unit
+val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
+val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
 val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 09a0ba83c..daec1191e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -483,8 +483,8 @@ type implicit_interactive_request =
 
 type implicit_discharge_request =
   | ImplLocal
-  | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of mutual_inductive * implicits_flags
+  | ImplConstant of Constant.t * implicits_flags
+  | ImplMutualInductive of MutInd.t * implicits_flags
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 4b78f54ea..658d9e01a 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -98,8 +98,8 @@ val compute_implicits_names : env -> types -> Name.t list
 (** {6 Computation of implicits (done using the global environment). } *)
 
 val declare_var_implicits : variable -> unit
-val declare_constant_implicits : constant -> unit
-val declare_mib_implicits : mutual_inductive -> unit
+val declare_constant_implicits : Constant.t -> unit
+val declare_mib_implicits : MutInd.t -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
diff --git a/interp/notation.ml b/interp/notation.ml
index d3cac1e3e..076570c8a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -234,7 +234,7 @@ let find_delimiters_scope ?loc key =
 
 type interp_rule =
   | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
+  | SynDefRule of KerName.t
 
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 75c8d5aa5..e312a3767 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -110,7 +110,7 @@ val availability_of_prim_token :
 (** Binds a notation in a given scope to an interpretation *)
 type interp_rule =
   | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
+  | SynDefRule of KerName.t
 
 val declare_notation_interpretation : notation -> scope_name option ->
       interpretation -> notation_location -> onlyprint:bool -> unit
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 36a3986b5..4d2cb5b74 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,4 +16,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 val declare_syntactic_definition : bool -> Id.t ->
   Flags.compat_version option -> syndef_interpretation -> unit
 
-val search_syntactic_definition : kernel_name -> syndef_interpretation
+val search_syntactic_definition : KerName.t -> syndef_interpretation