From 1c186562c2fc628d9ec4b6cda888750a642da117 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 5 Jan 2015 16:33:20 +0100
Subject: 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.
---
 library/declare.ml  | 10 +++++-----
 library/declare.mli |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'library')

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