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

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

checker/cic.mli

@@ -81,7 +81,7 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 type 'a puniverses = 'a Univ.puniverses
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -127,12 +127,12 @@ type section_context = unit
 
 type delta_hint =
   | Inline of int * constr option
-  | Equiv of kernel_name
+  | Equiv of KerName.t
 
-type delta_resolver = module_path MPmap.t * delta_hint KNmap.t
+type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
 
 type 'a umap_t = 'a MPmap.t * 'a MBImap.t
-type substitution = (module_path * delta_resolver) umap_t
+type substitution = (ModPath.t * delta_resolver) umap_t
 
 (** {6 Delayed constr} *)
 
@@ -194,7 +194,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : mutual_inductive;
+  proj_ind : MutInd.t;
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
@@ -241,7 +241,7 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * constant array * projection_body array) option
+type record_body = (Id.t * Constant.t array * projection_body array) option
     (* The body is empty for non-primitive records, otherwise we get its
        binder name in projections and list of projections if it is primitive. *)
 
@@ -347,12 +347,12 @@ type ('ty,'a) functorize =
     only for short module printing and for extraction. *)
 
 type with_declaration =
-  | WithMod of Id.t list * module_path
+  | WithMod of Id.t list * ModPath.t
   | WithDef of Id.t list * (constr * Univ.universe_context)
 
 type module_alg_expr =
-  | MEident of module_path
-  | MEapply of module_alg_expr * module_path
+  | MEident of ModPath.t
+  | MEapply of module_alg_expr * ModPath.t
   | MEwith of module_alg_expr * with_declaration
 
 (** A component of a module structure *)
@@ -386,7 +386,7 @@ and module_implementation =
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and 'a generic_module_body =
-  { mod_mp : module_path; (** absolute path of the module *)
+  { mod_mp : ModPath.t; (** absolute path of the module *)
     mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)

checker/closure.ml

@@ -63,7 +63,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
@@ -86,7 +86,7 @@ module RedFlags = (struct
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
-	      | CONST of constant | VAR of Id.t
+	      | CONST of Constant.t | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fIOTA = IOTA
@@ -165,7 +165,7 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of int
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 module KeyHash =
 struct
@@ -281,9 +281,9 @@ and fterm =
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *)
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs

checker/closure.mli

@@ -30,7 +30,7 @@ val all_opaque      : transparent_state
 val all_transparent : transparent_state
 
 val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> constant -> bool
+val is_transparent_constant : transparent_state -> Constant.t -> bool
 
 (* Sets of reduction kinds. *)
 module type RedFlagsSig = sig
@@ -42,7 +42,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
 
   (* No reduction at all *)
@@ -71,7 +71,7 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of int
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
@@ -100,9 +100,9 @@ type fterm =
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
@@ -142,7 +142,7 @@ val inject : constr -> fconstr
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
 val destFLambda :
-  (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
+  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
 
 (* Global and local constant cache *)
 type clos_infos

checker/declarations.mli

@@ -34,12 +34,12 @@ val empty_delta_resolver : delta_resolver
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
-val add_mbid : MBId.t -> module_path -> substitution -> substitution
-val add_mp   : module_path -> module_path -> substitution -> substitution
-val map_mbid : MBId.t -> module_path -> substitution
-val map_mp   : module_path -> module_path -> substitution
-val mp_in_delta : module_path -> delta_resolver -> bool
-val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
+val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution
+val add_mp   : ModPath.t -> ModPath.t -> substitution -> substitution
+val map_mbid : MBId.t -> ModPath.t -> substitution
+val map_mp   : ModPath.t -> ModPath.t -> substitution
+val mp_in_delta : ModPath.t -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun

checker/environ.ml

@@ -8,7 +8,7 @@ open Declarations
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name  KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 

checker/environ.mli

@@ -6,7 +6,7 @@ open Cic
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
@@ -34,7 +34,7 @@ val rel_context : env -> rel_context
 val lookup_rel : int -> env -> rel_declaration
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
-val push_rec_types : name array * constr array * 'a -> env -> env
+val push_rec_types : Name.t array * constr array * 'a -> env -> env
 
 (* Universes *)
 val universes : env -> Univ.universes
@@ -44,31 +44,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
-val lookup_constant : constant -> env -> Cic.constant_body
-val add_constant : constant -> Cic.constant_body -> env -> env
-val constant_type : env -> constant puniverses -> constr Univ.constrained
+val lookup_constant : Constant.t -> env -> Cic.constant_body
+val add_constant : Constant.t -> Cic.constant_body -> env -> env
+val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
 type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant puniverses -> constr
-val evaluable_constant : constant -> env -> bool
+val constant_value : env -> Constant.t puniverses -> constr
+val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : constant -> env -> bool
+val is_projection : Constant.t -> env -> bool
 val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
 
 val lookup_mind :
-  mutual_inductive -> env -> Cic.mutual_inductive_body
+  MutInd.t -> env -> Cic.mutual_inductive_body
 
 val add_mind :
-  mutual_inductive -> Cic.mutual_inductive_body -> env -> env
+  MutInd.t -> Cic.mutual_inductive_body -> env -> env
 
 (* Modules *)
 val add_modtype :
-  module_path -> Cic.module_type_body -> env -> env
+  ModPath.t -> Cic.module_type_body -> env -> env
 val shallow_add_module :
-  module_path -> Cic.module_body -> env -> env
-val shallow_remove_module : module_path -> env -> env
-val lookup_module : module_path -> env -> Cic.module_body
-val lookup_modtype : module_path -> env -> Cic.module_type_body
+  ModPath.t -> Cic.module_body -> env -> env
+val shallow_remove_module : ModPath.t -> env -> env
+val lookup_module : ModPath.t -> env -> Cic.module_body
+val lookup_modtype : ModPath.t -> env -> Cic.module_type_body

checker/indtypes.mli

@@ -12,8 +12,8 @@ open Cic
 open Environ
 (*i*)
 
-val prkn : kernel_name -> Pp.t
-val prcon : constant -> Pp.t
+val prkn : KerName.t -> Pp.t
+val prcon : Constant.t -> Pp.t
 
 (*s The different kinds of errors that may result of a malformed inductive
   definition. *)
@@ -34,4 +34,4 @@ exception InductiveError of inductive_error
 
 (*s The following function does checks on inductive declarations. *)
 
-val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env
+val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env

checker/inductive.mli

@@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr
 (* Return type as quoted by the user *)
 val type_of_constructor : pconstructor -> mind_specif -> constr
 
-val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array
+val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:

checker/mod_checking.mli

@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit
+val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit

checker/modops.mli

@@ -15,7 +15,7 @@ open Environ
 (* Various operations on modules and module types *)
 
 val module_type_of_module :
-  module_path option -> module_body -> module_type_body
+  ModPath.t option -> module_body -> module_type_body
 
 val is_functor : ('ty,'a) functorize -> bool
 
@@ -24,24 +24,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
-val add_module_type : module_path -> module_type_body -> env -> env
+val add_module_type : ModPath.t -> module_type_body -> env -> env
 
-val strengthen : module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> ModPath.t -> module_type_body
 
-val subst_and_strengthen : module_body -> module_path -> module_body
+val subst_and_strengthen : module_body -> ModPath.t -> module_body
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
-val error_not_match : label -> structure_field_body -> 'a
+val error_not_match : Label.t -> structure_field_body -> 'a
 
 val error_with_module : unit -> 'a
 
-val error_no_such_label : label -> 'a
+val error_no_such_label : Label.t -> 'a
 
 val error_no_such_label_sub :
-  label -> module_path -> 'a
+  Label.t -> ModPath.t -> 'a
 
-val error_not_a_constant : label -> 'a
+val error_not_a_constant : Label.t -> 'a
 
-val error_not_a_module : label -> 'a
+val error_not_a_module : Label.t -> 'a

checker/term.mli

@@ -38,8 +38,8 @@ val fold_rel_context_outside :
 val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
-val compose_lam : (name * constr) list -> constr -> constr
-val decompose_lam : constr -> (name * constr) list * constr
+val compose_lam : (Name.t * constr) list -> constr -> constr
+val decompose_lam : constr -> (Name.t * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr

checker/type_errors.ml

@@ -52,14 +52,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error

checker/type_errors.mli

@@ -54,14 +54,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
@@ -96,9 +96,9 @@ val error_cant_apply_bad_type :
       unsafe_judgment -> unsafe_judgment array -> 'a
 
 val error_ill_formed_rec_body :
-  env -> guard_error -> name array -> int -> 'a
+  env -> guard_error -> Name.t array -> int -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array -> constr array -> 'a
+  env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a
 
 val error_unsatisfied_constraints : env -> Univ.constraints -> 'a

checker/values.ml

@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
+MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli
 
 *)