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

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

6 files changed, 18 insertions, 18 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 4dbf6c18a..a4ad233b0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -99,8 +99,8 @@ val mkProd : Name.t * t * t -> t
 val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
-val mkConst : constant -> t
-val mkConstU : constant * EInstance.t -> t
+val mkConst : Constant.t -> t
+val mkConstU : Constant.t * EInstance.t -> t
 val mkProj : (projection * t) -> t
 val mkInd : inductive -> t
 val mkIndU : inductive * EInstance.t -> t
@@ -157,7 +157,7 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
 val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
 val destApp : Evd.evar_map -> t -> t * t array
-val destConst : Evd.evar_map -> t -> constant * EInstance.t
+val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
diff --git a/engine/evd.mli b/engine/evd.mli
index 96e4b6acc..7576b3d5f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -580,7 +580,7 @@ val update_sigma_env : evar_map -> env -> evar_map
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c548fc4ac..ff0b5a74e 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -61,9 +61,9 @@ let is_imported_ref = function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
-      let (mp,_,_) = repr_mind kn in is_imported_modpath mp
+      let (mp,_,_) = MutInd.repr3 kn in is_imported_modpath mp
   | ConstRef kn ->
-      let (mp,_,_) = repr_con kn in is_imported_modpath mp
+      let (mp,_,_) = Constant.repr3 kn in is_imported_modpath mp
 
 let is_global id =
   try
@@ -99,7 +99,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
     match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
-    | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
+    | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
     | Const _ | Ind _ | Construct _ | Var _ as c ->
 	Some (basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -130,8 +130,8 @@ let hdchar env sigma c =
     match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
     | Cast (c,_,_) | App (c,_) -> hdrec k c
-    | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
-    | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
+    | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
+    | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
     | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
diff --git a/engine/termops.ml b/engine/termops.ml
index 76f707f94..67533cce4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -31,7 +31,7 @@ let pr_sort_family = function
   | InProp -> (str "Prop")
   | InType -> (str "Type")
 
-let pr_con sp = str(string_of_con sp)
+let pr_con sp = str(Constant.to_string sp)
 
 let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
   let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
@@ -74,9 +74,9 @@ let rec pr_constr c = match kind_of_term c with
       (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
-  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
+  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
   | Construct (((sp,i),j),u) ->
-      str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+      str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
   | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
   | Case (ci,p,c,bl) -> v 0
       (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
diff --git a/engine/universes.ml b/engine/universes.ml
index 7f5bf24b7..0a2045a04 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -161,7 +161,7 @@ let compare_head_gen_proj env equ eqs eqc' m n =
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
       (match kind_of_term f with
-      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
           let pb = Environ.lookup_projection p env in
           let npars = pb.Declarations.proj_npars in
 	  if Array.length args == npars + 1 then
diff --git a/engine/universes.mli b/engine/universes.mli
index 8b2217d44..3678ec94d 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -31,10 +31,10 @@ val set_remote_new_univ_level : universe_level RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_level : Names.dir_path -> universe_level
-val new_univ : Names.dir_path -> universe
-val new_Type : Names.dir_path -> types
-val new_Type_sort : Names.dir_path -> sorts
+val new_univ_level : DirPath.t -> universe_level
+val new_univ : DirPath.t -> universe
+val new_Type : DirPath.t -> types
+val new_Type_sort : DirPath.t -> sorts
 
 val new_global_univ : unit -> universe in_universe_context_set
 val new_sort_in_family : sorts_family -> sorts
@@ -90,7 +90,7 @@ val fresh_instance_from : abstract_universe_context -> universe_instance option
 
 val fresh_sort_in_family : env -> sorts_family -> 
   sorts in_universe_context_set
-val fresh_constant_instance : env -> constant ->
+val fresh_constant_instance : env -> Constant.t ->
   pconstant in_universe_context_set
 val fresh_inductive_instance : env -> inductive ->
   pinductive in_universe_context_set