diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 7f2887f200..e57c4d295e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -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 } val mind_type_finite : mutual_inductive_body -> int -> bool |