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.
---
 kernel/indtypes.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel')

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