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.

---
 kernel/entries.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/entries.mli')

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