diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2aedc8dfd0..cb4b3f6556 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -31,7 +31,9 @@ type mutual_inductive_body = { mind_singl : constr option; mind_nparams : int } -type mutual_inductive_entry = section_path * mutual_inductive_body +type mutual_inductive_entry = { + mind_entry_params : (identifier * constr) list; + mind_entry_inds : (identifier * constr * (identifier * constr) list) list } let mind_type_finite mib i = mib.mind_packets.(i).mind_finite |