kernel/ind Change interface of declare_mind and declare_mutual

Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.

8 files changed, 31 insertions, 17 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 61ce63f1bb..481e333cca 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -782,7 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
   let pkt = packets.(0) in	  
   let isrecord = 
     match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
+    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
 	if p then 
diff --git a/library/declare.ml b/library/declare.ml
index 56c789c1ed..9e94b150eb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -389,20 +389,20 @@ let declare_projections mind =
 	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent) 
 	in
-	  assert(eq_constant kn kn')) kns
-    | Some None | None -> ()
+	  assert(eq_constant kn kn')) kns; true
+    | Some None | None -> false
 
 (* for initial declaration *)
-let declare_mind isrecord mie =
+let declare_mind mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
-  declare_projections mind;
+  let isprim = declare_projections mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
-  oname
+  oname, isprim
 
 (* Declaration messages *)
 
diff --git a/library/declare.mli b/library/declare.mli
index bda90229e6..5be8a5563f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -67,8 +67,8 @@ val set_declare_scheme :
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
-   the whole block (boolean must be true iff it is a record) *)
-val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
+   the whole block and a boolean indicating if it is a primitive record. *)
+val declare_mind : mutual_inductive_entry -> object_name * bool
 
 (** Declaration messages *)
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 8e3c0ba9c2..93b9725e50 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let mie,impls = Command.interp_mutual_inductive indl [] 
           false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
+  ignore (Command.declare_mutual_inductive_with_eliminations mie impls)
 
 
 (* Find infos on identifier id. *)
diff --git a/test-suite/bugs/closed/3899.v b/test-suite/bugs/closed/3899.v
new file mode 100644
index 0000000000..e83166aaec
--- /dev/null
+++ b/test-suite/bugs/closed/3899.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+Record unit : Set := tt {}.
+Fail Check fun x : unit => eq_refl : tt = x.
+Fail Check fun x : unit => eq_refl : x = tt.
+Fail Check fun x y : unit => (eq_refl : x = tt) : x = y.
+Fail Check fun x y : unit => eq_refl : x = y.
+
+Record ok : Set := tt' { a : unit }.
+
+Record nonprim : Prop := { undef : unit }.
+Record prim : Prop := { def : True }.
\ No newline at end of file
diff --git a/toplevel/command.ml b/toplevel/command.ml
index cd5aa7528e..7c5f8a4578 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -294,9 +294,10 @@ type structured_one_inductive_expr = {
 type structured_inductive_expr =
   local_binder list * structured_one_inductive_expr list
 
-let minductive_message = function
+let minductive_message warn = function
   | []  -> error "No inductive definition."
-  | [x] -> (pr_id x ++ str " is defined")
+  | [x] -> (pr_id x ++ str " is defined" ++ 
+	    if warn then str " as a non-primitive record" else mt())
   | l   -> hov 0  (prlist_with_sep pr_comma pr_id l ++
 		     spc () ++ str "are defined")
 
@@ -599,7 +600,7 @@ let is_recursive mie =
       List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
   | _ -> false
 
-let declare_mutual_inductive_with_eliminations isrecord mie impls =
+let declare_mutual_inductive_with_eliminations mie impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
@@ -612,7 +613,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
   | _ -> ()
   end;
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_,kn) = declare_mind isrecord mie in
+  let (_, kn), prim = declare_mind mie in
   let mind = Global.mind_of_delta_kn kn in
   List.iteri (fun i (indimpls, constrimpls) ->
 		   let ind = (mind,i) in
@@ -622,7 +623,8 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
 			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 		       constrimpls)
       impls;
-  if_verbose msg_info (minductive_message names);
+  let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
+  if_verbose msg_info (minductive_message warn_prim names);
   if mie.mind_entry_private == None
   then declare_default_schemes mind;
   mind
@@ -636,7 +638,7 @@ let do_mutual_inductive indl poly prv finite =
   (* Interpret the types *)
   let mie,impls = interp_mutual_inductive indl ntns poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
+  ignore (declare_mutual_inductive_with_eliminations mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index bd6da2dbed..f01bc27803 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -97,7 +97,7 @@ val interp_mutual_inductive :
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
-  Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list ->
+  mutual_inductive_entry -> one_inductive_impls list ->
   mutual_inductive
 
 (** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4ccf794492..9c2ad11102 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -366,7 +366,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
       mind_entry_universes = ctx } in
-  let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in