diff options
Diffstat (limited to 'checker/cic.mli')
-rw-r--r-- | checker/cic.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 3304b032e..4846a9af8 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. } *) @@ -207,7 +206,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) @@ -252,9 +251,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 * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : constr; @@ -322,7 +322,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 *) |