[api] Deprecate all legacy uses of Name.Id in core.

This is a first step towards some of the solutions proposed in #6008.

8 files changed, 34 insertions, 34 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index d111dd3c0..d97fd2b3a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -546,28 +546,28 @@ val eq_ind_chk : inductive -> inductive -> bool
 (** {5 Identifiers} *)
 
 type identifier = Id.t
-(** @deprecated Alias for [Id.t] *)
+[@@ocaml.deprecated "Alias for [Id.t]"]
 
-val string_of_id : identifier -> string
-(** @deprecated Same as [Id.to_string]. *)
+val string_of_id : Id.t -> string
+[@@ocaml.deprecated "Same as [Id.to_string]."]
 
-val id_of_string : string -> identifier
-(** @deprecated Same as [Id.of_string]. *)
+val id_of_string : string -> Id.t
+[@@ocaml.deprecated "Same as [Id.of_string]."]
 
-val id_ord : identifier -> identifier -> int
-(** @deprecated Same as [Id.compare]. *)
+val id_ord : Id.t -> Id.t -> int
+[@@ocaml.deprecated "Same as [Id.compare]."]
 
-val id_eq : identifier -> identifier -> bool
-(** @deprecated Same as [Id.equal]. *)
+val id_eq : Id.t -> Id.t -> bool
+[@@ocaml.deprecated "Same as [Id.equal]."]
 
-module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
-(** @deprecated Same as [Id.Set]. *)
+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 = identifier and type t = Id.Pred.t
-(** @deprecated Same as [Id.Pred]. *)
+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
-(** @deprecated Same as [Id.Map]. *)
+[@@ocaml.deprecated "Same as [Id.Map]."]
 
 (** {5 Directory paths} *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index e08d913bc..6e9991ac5 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -59,7 +59,7 @@ type gname =
   | Gnormtbl of label option * int
   | Ginternal of string
   | Grel of int
-  | Gnamed of identifier
+  | Gnamed of Id.t
 
 let eq_gname gn1 gn2 =
   match gn1, gn2 with
@@ -266,7 +266,7 @@ type primitive =
   | Mk_fix of rec_pos * int 
   | Mk_cofix of int
   | Mk_rel of int
-  | Mk_var of identifier
+  | Mk_var of Id.t
   | Mk_proj
   | Is_accu
   | Is_int
@@ -625,7 +625,7 @@ let decompose_MLlam c =
 
 (*s Global declaration *)
 type global =
-(*  | Gtblname of gname * identifier array *)
+(*  | Gtblname of gname * Id.t array *)
   | Gtblnorm of gname * lname array * mllambda array 
   | Gtblfixtype of gname * lname array * mllambda array
   | Glet of gname * mllambda
@@ -732,7 +732,7 @@ type env =
       env_bound : int; (* length of env_rel *)
       (* free variables *)
       env_urel : (int * mllambda) list ref; (* list of unbound rel *)
-      env_named : (identifier * mllambda) list ref;
+      env_named : (Id.t * mllambda) list ref;
       env_univ : lname option}
 
 let empty_env univ () =
@@ -1955,8 +1955,8 @@ let is_code_loaded ~interactive name =
       if is_loaded_native_file s then true
       else (name := NotLinked; false)
 
-let param_name = Name (id_of_string "params")
-let arg_name = Name (id_of_string "arg")
+let param_name = Name (Id.of_string "params")
+let arg_name = Name (Id.of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
   let u = Declareops.inductive_polymorphic_context mb in
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 2353470f0..73f18f7a7 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -21,7 +21,7 @@ type uint =
 
 and lambda =
   | Lrel          of name * int 
-  | Lvar          of identifier
+  | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
   | Levar         of existential * lambda (* type *)
   | Lprod         of lambda * lambda 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 7463a30fe..1c9996d89 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -52,7 +52,7 @@ type atom =
   | Aconstant of pconstant
   | Aind of pinductive
   | Asort of sorts
-  | Avar of identifier
+  | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t)
   | Afix of t array * t array * rec_pos * int
             (* types, bodies, rec_pos, pos *)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 49b1e122d..0e2db8486 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -44,7 +44,7 @@ type atom =
   | Aconstant of pconstant
   | Aind of pinductive
   | Asort of sorts
-  | Avar of identifier
+  | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t) 
   | Afix of t array * t array * rec_pos * int 
   | Acofix of t array * t array * int * t
@@ -62,7 +62,7 @@ val mk_rels_accu : int -> int -> t array
 val mk_constant_accu : constant -> Univ.Level.t array -> t
 val mk_ind_accu : inductive -> Univ.Level.t array -> t
 val mk_sort_accu : sorts -> Univ.Level.t array -> t
-val mk_var_accu : identifier -> t
+val mk_var_accu : Id.t -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
 val mk_prod_accu : name -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f93b24b3e..e28c8e826 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -385,10 +385,10 @@ let build_constant_declaration kn env result =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
-      let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
+      let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
       let n = List.length l in
-      let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in
-      let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in
+      let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
+      let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
       let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
       user_err Pp.(prlist str
          ["The following section "; (String.plural n "variable"); " ";
@@ -414,7 +414,7 @@ let build_constant_declaration kn env result =
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set env typ in
         let ids_def = match def with
-        | Undef _ -> Idset.empty
+        | Undef _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
             let vars =
@@ -425,7 +425,7 @@ let build_constant_declaration kn env result =
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
-        keep_hyps env (Idset.union ids_typ ids_def), def
+        keep_hyps env (Id.Set.union ids_typ ids_def), def
     | None ->
         if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty;
@@ -438,14 +438,14 @@ let build_constant_declaration kn env result =
         | Def cs as x ->
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
               let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
               check declared inferred) lc) in
   let univs = result.cook_universes in
   let tps = 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index bbaf569d3..9813fc566 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -44,7 +44,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of identifier * 'constr
+  | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 1b2ccf8f8..95a963da2 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -45,7 +45,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of identifier * 'constr
+  | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -74,7 +74,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
 
-val error_reference_variables : env -> identifier -> constr -> 'a
+val error_reference_variables : env -> Id.t -> constr -> 'a
 
 val error_elim_arity :
   env -> pinductive -> sorts_family list -> constr -> unsafe_judgment ->