From 6007579ade085a60664e6b0d4596ff98c51aabf9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Apr 2018 16:07:37 +0200 Subject: Using more general information for primitive records. This brings more compatibility with handling of mutual primitive records in the kernel. --- kernel/entries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/entries.ml') diff --git a/kernel/entries.ml b/kernel/entries.ml index 3c555f8c7..724ed9ec7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -49,9 +49,9 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : (Id.t option) option; - (** Some (Some id): primitive record with id the binder name of the record - in projections. + mind_entry_record : (Id.t array option) option; + (** Some (Some ids): primitive records with ids the binder name of each + record in their respective projections. Not used by the kernel. Some None: non-primitive record *) mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; -- cgit v1.2.3