diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 0c8b15e3ce..65f70e2776 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -77,6 +77,8 @@ val mind_user_lc : one_inductive_body -> typed_type array val mind_user_arity : one_inductive_body -> typed_type val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body +val mind_arities_context : mutual_inductive_body -> rel_declaration list + (*s Declaration of inductive types. *) type mutual_inductive_entry = { |