Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field record

Reviewed-by: ejgallego

4 files changed, 17 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/bug_9595.v b/test-suite/bugs/closed/bug_9595.v
new file mode 100644
index 0000000000..312ed7d045
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9595.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+Set Warnings "+non-primitive-record".
+
+(* 0 fields *)
+Fail Record foo := { a := 0 }.
+
+(* anonymous field *)
+Fail Record foo := { _ : nat }.
+
+(* squashed *)
+Fail Record foo : Prop := { a : nat }.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 9bbfb8eec6..7fa99b25cb 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -529,7 +529,7 @@ let warn_non_primitive_record =
           (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++
                     strbrk" could not be defined as a primitive record")))
 
-let declare_mutual_inductive_with_eliminations mie pl impls =
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
@@ -543,8 +543,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_, kn), prim = declare_mind mie in
   let mind = Global.mind_of_delta_kn kn in
-  if match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false
-  then warn_non_primitive_record (mind,0);
+  if primitive_expected && not prim then warn_non_primitive_record (mind,0);
   Declare.declare_univ_binders (IndRef (mind,0)) pl;
   List.iteri (fun i (indimpls, constrimpls) ->
               let ind = (mind,i) in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 1d6f652385..224cce67ad 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -43,6 +43,7 @@ type one_inductive_impls =
   Impargs.manual_implicits list (* for constrs *)
 
 val declare_mutual_inductive_with_eliminations :
+  ?primitive_expected:bool ->
   mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
   MutInd.t
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 9c52ac4ee5..3202c9bed2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -416,8 +416,6 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
   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;
@@ -431,7 +429,9 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
   in
   let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
-  let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in
+  let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+      ~primitive_expected:!primitive_flag
+  in
   let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in