diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index f2d9ac9f5..82a2de094 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -25,7 +25,8 @@ type case_printing = type case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_ndecls : int array; (** number of real args of each constructor *) + ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*) + ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *) ci_pp_info : case_printing (** not interpreted by the kernel *) } |