diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cc1bb7f418..cea769955e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -58,6 +58,8 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array +val nconstructors : inductive -> int + (* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int |