diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9bb848c6a4..674d7a2a91 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -536,9 +536,13 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr let record_info = match isrecord with | Some (Some rid) -> let is_record pkt = - List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim - && Array.length pkt.mind_consnames == 1 - && pkt.mind_consnrealargs.(0) > 0 + if Array.length pkt.mind_consnames != 1 then + user_err ~hdr:"build_inductive" + Pp.(str "Primitive records must have exactly one constructor.") + else if pkt.mind_consnrealargs.(0) = 0 then + user_err ~hdr:"build_inductive" + Pp.(str "Primitive records must have at least one constructor argument.") + else List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim in (** The elimination criterion ensures that all projections can be defined. *) if Array.for_all is_record packets then |