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

diff --git a/library/declare.ml b/library/declare.ml
index f746282d14..bacd9e2c10 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;