Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive records

Reviewed-by: ppedrot

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;