diff options
Diffstat (limited to 'kernel/entries.mli')
| -rw-r--r-- | kernel/entries.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index edba6e608..e383dbabd 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -49,6 +49,7 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { + mind_entry_record : bool; mind_entry_finite : bool; mind_entry_inds : one_inductive_entry list } |