- 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, 7 insertions, 3 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0e4d6e3306..a675fe028c 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 3015eab25b..bd5218efff 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 d2aa48db92..896cc41c72 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;