diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 17c89ac93d..32d844e9a7 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,4 +1,12 @@ (* $Id$ *) -type mind +open Names + +type mind_entry + +type mutual_inductive_body + +type mutual_inductive_entry = section_path * mutual_inductive_body + +val mind_type_finite : mutual_inductive_body -> int -> bool |