diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-16 10:58:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 17:47:48 +0100 |
| commit | fba1f0ed91aff372234b5a95422ee18f1730522f (patch) | |
| tree | fa5ca22e0af3ad47067c5908385039e1668f7843 /checker/cic.mli | |
| parent | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (diff) | |
Update checker/values and cic due to changes in case_info and record_body.
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index f00c95705..6ed9a4d25 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -227,6 +227,10 @@ type recarg = type wf_paths = recarg Rtree.t +type record_body = (Id.t * constant 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 regular_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -288,9 +292,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : (constant array * projection_body array) option; - (** Whether the inductive type has been declared as a record, - In that case we get its canonical eta-expansion and list of projections. *) + mind_record : record_body option; (** Whether the inductive type has been declared as a record. *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) |