diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index d09cdbdb7..f877b5391 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -65,6 +65,10 @@ val type_case_branches : env -> inductive * constr list -> unsafe_judgment -> constr -> types array * types * constraints +val build_branches_type : + inductive -> mutual_inductive_body * one_inductive_body -> + constr list -> constr -> types array + (* Return the arity of an inductive type *) val mind_arity : one_inductive_body -> rel_context * sorts_family |