[api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`

6 files changed, 38 insertions, 38 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fdaeded87..f69c4bce7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -33,12 +33,12 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> Pp.t;
-  print_constant_with_infos : constant -> Pp.t;
+  print_inductive           : MutInd.t -> Pp.t;
+  print_constant_with_infos : Constant.t -> Pp.t;
   print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : kernel_name -> Pp.t;
-  print_module              : bool -> Names.module_path -> Pp.t;
-  print_modtype             : module_path -> Pp.t;
+  print_syntactic_def       : KerName.t -> Pp.t;
+  print_module              : bool -> ModPath.t -> Pp.t;
+  print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : Context.Named.Declaration.t -> Pp.t;
   print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
@@ -318,8 +318,8 @@ type locatable = Locatable : 'a locatable_info -> locatable
 type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
-  | Syntactic of kernel_name
-  | ModuleType of module_path
+  | Syntactic of KerName.t
+  | ModuleType of ModPath.t
   | Other : 'a * 'a locatable_info -> logical_name
   | Undefined of qualid
 
@@ -623,14 +623,14 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
              constraints *)
 	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-	  Some (print_constant with_values sep (constant_of_kn kn))
+	  Some (print_constant with_values sep (Constant.make1 kn))
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive (mind_of_kn kn))
+	  Some (gallina_print_inductive (MutInd.make1 kn))
       | (_,"MODULE") ->
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
       | (_,"MODULE TYPE") ->
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
@@ -750,12 +750,12 @@ let print_full_pure_context () =
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | "MODULE TYPE" ->
 	  (* TODO: make it reparsable *)
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index dbd101159..31fd766ea 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -80,12 +80,12 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> Pp.t;
-  print_constant_with_infos : constant -> Pp.t;
+  print_inductive           : MutInd.t -> Pp.t;
+  print_constant_with_infos : Constant.t -> Pp.t;
   print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : kernel_name -> Pp.t;
-  print_module              : bool -> Names.module_path -> Pp.t;
-  print_modtype             : module_path -> Pp.t;
+  print_syntactic_def       : KerName.t -> Pp.t;
+  print_module              : bool -> ModPath.t -> Pp.t;
+  print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : Context.Named.Declaration.t -> Pp.t;
   print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 70e96722d..e4bb89304 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -855,15 +855,15 @@ let prterm = pr_lconstr
    It is used primarily by the Print Assumptions command. *)
 
 type axiom =
-  | Constant of constant (* An axiom or a constant. *)
+  | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom * (Label.t * Context.Rel.t * types) list
-  | Opaque of constant     (* An opaque constant. *)
-  | Transparent of constant
+  | Opaque of Constant.t     (* An opaque constant. *)
+  | Transparent of Constant.t
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject =
@@ -873,11 +873,11 @@ struct
   let compare_axiom x y =
     match x,y with
     | Constant k1 , Constant k2 ->
-        con_ord k1 k2
+        Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
-        con_ord k1 k2
+        Constant.CanOrd.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
     | _ -> -1
@@ -890,10 +890,10 @@ struct
     | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2
     | Axiom _ , _ -> -1
     | _ , Axiom _ -> 1
-    | Opaque k1 , Opaque k2 -> con_ord k1 k2
+    | Opaque k1 , Opaque k2 -> Constant.CanOrd.compare k1 k2
     | Opaque _ , _ -> -1
     | _ , Opaque _ -> 1
-    | Transparent k1 , Transparent k2 -> con_ord k1 k2
+    | Transparent k1 , Transparent k2 -> Constant.CanOrd.compare k1 k2
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
@@ -907,8 +907,8 @@ let pr_assumptionset env s =
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
-	let mp,_,lab = repr_con kn in
-        str (string_of_mp mp) ++ str "." ++ pr_label lab
+	let mp,_,lab = Constant.repr3 kn in
+        str (ModPath.to_string mp) ++ str "." ++ Label.print lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ
@@ -942,7 +942,7 @@ let pr_assumptionset env s =
         let ax = pr_axiom env axiom typ ++
           cut() ++
           prlist_with_sep cut (fun (lbl, ctx, ty) ->
-            str " used in " ++ pr_label lbl ++
+            str " used in " ++ Label.print lbl ++
             str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
           l in
         (v, ax :: a, o, tr)
diff --git a/printing/printer.mli b/printing/printer.mli
index f55206f0d..e74f47efe 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -110,7 +110,7 @@ val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> Pp.t
 val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
 val pr_global              : global_reference -> Pp.t
 
-val pr_constant            : env -> constant -> Pp.t
+val pr_constant            : env -> Constant.t -> Pp.t
 val pr_existential_key     : evar_map -> existential_key -> Pp.t
 val pr_existential         : env -> evar_map -> existential -> Pp.t
 val pr_constructor         : env -> constructor -> Pp.t
@@ -183,15 +183,15 @@ val prterm                 : constr -> Pp.t (** = pr_lconstr *)
 
 (** Declarations for the "Print Assumption" command *)
 type axiom =
-  | Constant of constant (* An axiom or a constant. *)
+  | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom * (Label.t * Context.Rel.t * types) list
-  | Opaque of constant     (* An opaque constant. *)
-  | Transparent of constant
+  | Opaque of Constant.t     (* An opaque constant. *)
+  | Transparent of Constant.t
 
 module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : CMap.ExtS
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 755e905a7..d4b756346 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -301,7 +301,7 @@ let nametab_register_modparam mbid mtb =
       id
 
 let print_body is_impl env mp (l,body) =
-  let name = pr_label l in
+  let name = Label.print l in
   hov 2 (match body with
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 8c3f0149e..b0bbb21e0 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,6 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t
-val print_module : bool -> module_path -> Pp.t
-val print_modtype : module_path -> Pp.t
+val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val print_module : bool -> ModPath.t -> Pp.t
+val print_modtype : ModPath.t -> Pp.t