- 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.

3 files changed, 21 insertions, 13 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51b7b6f971..9d2382f6ec 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -223,8 +223,14 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
+let subst_mind_record sub (c, ps as r) =
+  let c' = subst_mps sub c in
+  let ps' = Array.smartmap (subst_constant sub) ps in
+    if c' == c && ps' == ps then r
+    else (c', ps')
+
 let subst_mind_body sub mib =
-  { mind_record = mib.mind_record ;
+  { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
diff --git a/kernel/entries.mli b/kernel/entries.mli
index c672ba731f..244637acda 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -41,7 +41,8 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
-  mind_entry_record : bool;
+  mind_entry_record : bool option; 
+  (** Some true: primitive record, Some false: non-primitive record *)
   mind_entry_finite : bool;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
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;