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

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

17 files changed, 40 insertions, 40 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index cbf5788e4..327ee0015 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -124,7 +124,7 @@ val prepare_predicate : ?loc:Loc.t ->
            (types * tomatch_type) list ->
            (rel_context * rel_context) list ->
            constr option ->
-           glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+           glob_constr option -> (Evd.evar_map * Name.t list * constr) list
 
-val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
   Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 260cd0444..fe969f9e5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -27,9 +27,9 @@ type cl_typ =
   | CL_SORT
   | CL_FUN
   | CL_SECVAR of variable
-  | CL_CONST of constant
+  | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of constant
+  | CL_PROJ of Constant.t
 
 type cl_info_typ = {
   cl_param : int
@@ -59,8 +59,8 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2
   | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8707078b5..b41d0efac 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -17,9 +17,9 @@ type cl_typ =
   | CL_SORT
   | CL_FUN
   | CL_SECVAR of variable
-  | CL_CONST of constant
+  | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of constant
+  | CL_PROJ of Constant.t
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ddef1cee9..b7b76c830 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -214,7 +214,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
   let convref ref c = 
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
-    | ConstRef c, Const (c',_) -> Names.eq_constant c c'
+    | ConstRef c, Const (c',_) -> Constant.equal c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
     | _, _ -> 
@@ -286,7 +286,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
 	(match c1, EConstr.kind sigma c2 with
-	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr))
+	| PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
 	    || Projection.unfolded pr ->
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
@@ -303,7 +303,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
       | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
-	when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> 
+	when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> 
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0f1a508c8..45fe2b2d8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -297,7 +297,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
     | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
@@ -341,7 +341,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 	  (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
     | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
@@ -771,7 +771,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    ise_try evd [f1; f2]
 	      
 	(* Catch the p.c ~= p c' cases *)
-	| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
+	| Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
 	  let res = 
 	    try Some (destApp evd (Retyping.expand_projection env evd p c []))
 	    with Retyping.RetypeError _ -> None
@@ -782,7 +782,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		(appr2,csts2)
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
-	| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
+	| Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
 	  let res = 
 	    try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
 	    with Retyping.RetypeError _ -> None
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index f27928662..9dd7068cb 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -64,7 +64,7 @@ val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_
     here by its relevant components [m] and [c]. It is used to
     interpret Ltac-bound names both in pretyping and printing of
     terms. *)
-val map_pattern_binders : (name -> name) ->
+val map_pattern_binders : (Name.t -> Name.t) ->
   tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
 
 (** [map_pattern f m c] applies [f] to the return predicate and the
@@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob
 
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
-val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name
+val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
 val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index aced42f83..0cb5974e8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -566,7 +566,7 @@ let build_mutual_induction_scheme env sigma = function
     	(List.map
 	   (function ((mind',u'),dep',s') ->
 	      let (sp',_) = mind' in
-	      if eq_mind sp sp' then
+	      if MutInd.equal sp sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		((mind',u'),mibi',mipi',dep',s')
 	      else
@@ -605,7 +605,7 @@ let lookup_eliminator ind_sp s =
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in
+    let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in
     let _ = Global.lookup_constant cst in
       ConstRef cst
   with Not_found ->
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa38d3b47..65d5161df 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -147,7 +147,7 @@ val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
 val get_constructors : env -> inductive_family -> constructor_summary array
-val get_projections  : env -> inductive_family -> constant array option
+val get_projections  : env -> inductive_family -> Constant.t array option
 
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index aaa946706..fd76a9473 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -174,7 +174,7 @@ let pattern_of_constr env sigma t =
          with
          | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
          | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
-    | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
+    | Const (sp,u)  -> PRef (ConstRef (Constant.make1 (Constant.canonical sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e970a1db9..4f4e49d82 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -37,7 +37,7 @@ type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : (Name.t * bool) list;
-  s_PROJ : constant option list }
+  s_PROJ : Constant.t option list }
 
 let structure_table =
   Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
@@ -48,7 +48,7 @@ let projection_table =
    is the inductive always (fst constructor) ? It seems so... *)
 
 type struc_tuple =
-    inductive * constructor * (Name.t * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -286,7 +286,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
 let discharge_canonical_structure (_,(cst,ind)) =
   Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
-let inCanonStruc : constant * inductive -> obj =
+let inCanonStruc : Constant.t * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 8e2333b34..066623164 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -20,10 +20,10 @@ type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : (Name.t * bool) list;
-  s_PROJ : constant option list }
+  s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    inductive * constructor * (Name.t * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 val declare_structure : struc_tuple -> unit
 
@@ -35,7 +35,7 @@ val lookup_structure : inductive -> struc_typ
 (** [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
-val lookup_projections : inductive -> constant option list
+val lookup_projections : inductive -> Constant.t option list
 
 (** raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2aa2f9013..308896f3a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -358,7 +358,7 @@ struct
        ++ str ")"
     | Proj (n,m,p,cst) ->
       str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
-	pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
+	pr_comma () ++ Constant.print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Termops.pr_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1828196fe..950fcdee4 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -258,7 +258,7 @@ val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixp
 val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
-val is_transparent : Environ.env -> constant tableKey -> bool
+val is_transparent : Environ.env -> Constant.t tableKey -> bool
 
 (** {6 Conversion Functions (uses closures, lazy strategy) } *)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9451b0f86..85383ba39 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -75,13 +75,13 @@ let global_of_evaluable_reference = function
   | EvalVarRef id -> VarRef id
 
 type evaluable_reference =
-  | EvalConst of constant
+  | EvalConst of Constant.t
   | EvalVar of Id.t
   | EvalRel of int
   | EvalEvar of EConstr.existential
 
 let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
-| EvalConst c1, EvalConst c2 -> eq_constant c1 c2
+| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
@@ -240,7 +240,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst kn ->
-	      Some (EvalConst (con_with_label kn (Label.of_id id))) in
+	      Some (EvalConst (Constant.change_label kn (Label.of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -521,7 +521,7 @@ let reduce_mind_case_use_function func env sigma mia =
 		       the block was indeed initially built as a global
 		       definition *)
                     let (kn, u) = destConst sigma func in
-                    let kn = con_with_label kn (Label.of_id id) in
+                    let kn = Constant.change_label kn (Label.of_id id) in
                     let cst = (kn, EInstance.kind sigma u) in
 		    try match constant_opt_value_in env cst with
 		      | None -> None
@@ -944,7 +944,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       | CoFix _ | Fix _ -> s'
       | Proj (p,t) when
 	  (match EConstr.kind sigma constr with
-	  | Const (c', _) -> eq_constant (Projection.constant p) c'
+	  | Const (c', _) -> Constant.equal (Projection.constant p) c'
 	  | _ -> false) ->
 	let pb = Environ.lookup_projection p env in
 	  if List.length stack <= pb.Declarations.proj_npars then
@@ -1050,7 +1050,7 @@ let contextually byhead occs f env sigma t =
 
 let match_constr_evaluable_ref sigma c evref = 
   match EConstr.kind sigma c, evref with
-  | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
+  | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 375a8a983..1e06e9f8c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -71,7 +71,7 @@ type typeclass = {
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
-	      * constant option) list;
+	      * Constant.t option) list;
   
   cl_strict : bool;
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 99cdbd3a3..20fbbb5a0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -36,7 +36,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8f7e2bba..01c28b5ed 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -554,10 +554,10 @@ let oracle_order env cf1 cf2 =
       | Some k2 ->
 	match k1, k2 with
 	| IsProj (p, _), IsKey (ConstKey (p',_)) 
-	  when eq_constant (Projection.constant p) p' -> 
+	  when Constant.equal (Projection.constant p) p' -> 
 	  Some (not (Projection.unfolded p))
 	| IsKey (ConstKey (p,_)), IsProj (p', _) 
-	  when eq_constant p (Projection.constant p') -> 
+	  when Constant.equal p (Projection.constant p') -> 
 	  Some (Projection.unfolded p')
 	| _ ->
           Some (Conv_oracle.oracle_order (fun x -> x)
@@ -784,7 +784,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
 	(** Fast path for projections. *)
-	| Proj (p1,c1), Proj (p2,c2) when eq_constant
+	| Proj (p1,c1), Proj (p2,c2) when Constant.equal
 	    (Projection.constant p1) (Projection.constant p2) ->
 	  (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
 	       substn c1 c2