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

7 files changed, 29 insertions, 17 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51b7b6f97..9d2382f6e 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 c672ba731..244637acd 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 6e87a0444..9c83ba1a9 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;
diff --git a/library/declare.ml b/library/declare.ml
index f746282d1..bacd9e2c1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -366,7 +366,7 @@ let dummy_one_inductive_entry mie = {
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
-  mind_entry_record = false;
+  mind_entry_record = None;
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0e4d6e330..a675fe028 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -525,7 +525,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   in
   (* Build the mutual inductive entry *)
   { mind_entry_params = List.map prepare_param ctx_params;
-    mind_entry_record = false;
+    mind_entry_record = None;
     mind_entry_finite = finite;
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 3015eab25..bd5218eff 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -91,7 +91,11 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let univs = Univ.UContext.union abs_ctx mib.mind_universes in
-  { mind_entry_record = mib.mind_record <> None;
+  let record = match mib.mind_record with
+    | None -> None
+    | Some (_, a) -> Some (Array.length a > 0)
+  in
+  { mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params';
     mind_entry_inds = inds';
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d2aa48db9..896cc41c7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -330,7 +330,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
   end;
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_record = true;
+      mind_entry_record = Some !primitive_flag;
       mind_entry_finite = finite != CoFinite;
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;