diff options
| -rw-r--r-- | kernel/indtypes.ml | 10 | ||||
| -rw-r--r-- | vernac/record.ml | 8 |
2 files changed, 14 insertions, 4 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 diff --git a/vernac/record.ml b/vernac/record.ml index 1b7b828f47..ed5edb7e3b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -414,9 +414,15 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in + let primitive = + !primitive_flag && + List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + (* will warn_non_primitive_record in declare_projections if we try + to declare a 0-field record *) + in let mie = { mind_entry_params = params; - mind_entry_record = Some (if !primitive_flag then Some binder_name else None); + mind_entry_record = Some (if primitive then Some binder_name else None); mind_entry_finite = finite; mind_entry_inds = blocks; mind_entry_private = None; |