diff options
| author | Pierre-Marie Pédrot | 2019-02-05 15:56:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 15:56:36 +0100 |
| commit | b307529a3888ab632b7076a793904d150d263eac (patch) | |
| tree | 105892da79735e63bb59f8ae1089fabcb0adbaa0 /kernel | |
| parent | 38b1682ee6b6342ca582bac4e658f7d1c3919de4 (diff) | |
| parent | 5531d049b2a4f4c6c9e55ad31acae5b31aeda5c5 (diff) | |
Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive records
Reviewed-by: ppedrot
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 |