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 4c5c58a9f2..23d0a32ca5 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -42,6 +42,8 @@ val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr val mis_constr_nargs : inductive -> int array +val mis_constr_nargs_env : env -> inductive -> int array + type constructor_summary = { cs_cstr : constructor; cs_params : constr list; |