From 31f333031b66f7afdfc35662aca9f9f40bbccbd0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Feb 2019 14:41:55 +0100
Subject: Fix #9595: missing non-primitive-record warning with 0 field record

---
 vernac/comInductive.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3