From 3f7f3a9bc9fde8e1d44d1179fa8dd16221ebf526 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 25 Jul 2014 17:52:46 +0200
Subject: - Do module substitution inside mind_record. - Distinguish between
 primitive and non-primitive records in the kernel declaration, so as to try
 eta-conversion on primitive records only.

---
 kernel/indtypes.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6e87a04446..9c83ba1a98 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -742,17 +742,18 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       } in
   let packets = Array.map2 build_one_packet inds recargs in
   let isrecord = 
-    let pkt = packets.(0) in
-      if isrecord (* || (Array.length pkt.mind_consnames = 1 &&  *)
-        (* inductive_sort_family pkt <> InProp) *) then
-	let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
-	let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in
-	try 
-	  let exp = compute_expansion ((kn, 0), u) params 
-	    (List.firstn pkt.mind_consnrealdecls.(0) rctx) 
-	  in Some exp
-	with UndefinableExpansion -> None
-      else None
+    match isrecord with
+    | Some true -> (* || (Array.length pkt.mind_consnames = 1 &&  *)
+      let pkt = packets.(0) in	  
+      let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
+      let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in
+	(try 
+	 let exp = compute_expansion ((kn, 0), u) params 
+	   (List.firstn pkt.mind_consnrealdecls.(0) rctx) 
+	 in Some exp
+	 with UndefinableExpansion -> (Some (mkProp, [||])))
+    | Some false -> Some (mkProp, [||])
+    | None -> None
   in
     (* Build the mutual inductive *)
     { mind_record = isrecord;
-- 
cgit v1.2.3