From 3f7f3a9bc9fde8e1d44d1179fa8dd16221ebf526 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 25 Jul 2014 17:52:46 +0200
Subject: - 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.

---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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;
-- 
cgit v1.2.3