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

1 files changed, 2 insertions, 1 deletions

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;