diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 32 |
1 files changed, 10 insertions, 22 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index c4b00d0d..17259bb4 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -33,11 +33,10 @@ open Names (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type sorts = - | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) + | Prop + | Set + | Type of Univ.universe (** {6 The sorts family of CCI. } *) @@ -128,7 +127,7 @@ type section_context = unit (** {6 Substitutions} *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t @@ -203,18 +202,6 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) -(** Projections are a particular kind of constant: - always transparent. *) - -type projection_body = { - proj_ind : MutInd.t; - proj_npars : int; - proj_arg : int; - proj_type : constr; (* Type under params *) - proj_eta : constr * constr; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility, the match version *) -} - type constant_def = | Undef of inline | Def of constr_substituted @@ -233,6 +220,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } type constant_body = { @@ -241,7 +229,6 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : projection_body option; const_inline_code : bool; const_typing_flags : typing_flags; } @@ -255,9 +242,10 @@ type recarg = type wf_paths = recarg Rtree.t -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. *) +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Label.t array * constr array) array type regular_inductive_arity = { mind_user_arity : constr; @@ -325,7 +313,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** Whether the inductive type has been declared as a record. *) + mind_record : record_info; (** Whether the inductive type has been declared as a record. *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) |