diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd7d6c9c..95078800e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -50,7 +50,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) @@ -80,7 +80,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) type constant_body = { - const_hyps : Context.Named.t; (** New: younger hyp at top *) + const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; @@ -109,13 +109,22 @@ v} *) (** Record information: - If the record is not primitive, then None - Otherwise, we get: + If the type is not a record, then NotRecord + If the type is a non-primitive record, then FakeRecord + If it is a primitive record, for every type in the block, we get: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - - The checked projection bodies. *) + - The checked projection bodies. -type record_body = (Id.t * Constant.t array * projection_body array) option + The kernel does not exploit the difference between [NotRecord] and + [FakeRecord]. It is mostly used by extraction, and should be extruded from + the kernel at some point. +*) + +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : types; @@ -129,7 +138,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -181,19 +190,19 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** The record information *) + mind_record : record_info; (** The record information *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) + mind_hyps : Constr.named_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) |