diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1008492825..5551742c02 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -53,9 +53,9 @@ type 'a constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) -type constant_universes = - | Monomorphic_const of Univ.ContextSet.t - | Polymorphic_const of Univ.AUContext.t +type universes = + | Monomorphic of Univ.ContextSet.t + | Polymorphic of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -91,8 +91,9 @@ type constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : Constr.t Mod_subst.substituted constant_def; const_type : types; + const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; - const_universes : constant_universes; + const_universes : universes; const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which @@ -133,7 +134,7 @@ v} type record_info = | NotRecord | FakeRecord -| PrimRecord of (Id.t * Label.t array * types array) array +| PrimRecord of (Id.t * Label.t array * Sorts.relevance array * types array) array type regular_inductive_arity = { mind_user_arity : types; @@ -166,7 +167,7 @@ type one_inductive_body = { mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) + mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) *) @@ -176,6 +177,8 @@ type one_inductive_body = { mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) + mind_relevance : Sorts.relevance; + (** {8 Datas for bytecode compilation } *) mind_nb_constant : int; (** number of constant constructor *) @@ -185,11 +188,6 @@ type one_inductive_body = { mind_reloc_tbl : Vmvalues.reloc_table; } -type abstract_inductive_universes = - | Monomorphic_ind of Univ.ContextSet.t - | Polymorphic_ind of Univ.AUContext.t - | Cumulative_ind of Univ.ACumulativityInfo.t - type recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) @@ -213,7 +211,9 @@ type mutual_inductive_body = { 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 *) + mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) |