diff options
| -rw-r--r-- | kernel/constr.ml | 14 | ||||
| -rw-r--r-- | kernel/constr.mli | 14 |
2 files changed, 18 insertions, 10 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 753d18845..c3aebada2 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -42,11 +42,15 @@ type case_printing = cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *) style : case_style } type case_info = - { ci_ind : inductive; - ci_npar : int; - 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 *) + { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) + ci_npar : int; (* number of parameters of the above inductive type *) + ci_cstr_ndecls : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (with let's) *) + ci_cstr_nargs : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (w/o let's) *) + ci_pp_info : case_printing (* not interpreted by the kernel *) } (********************************************************************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 70f169931..edd4eb231 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -32,11 +32,15 @@ type case_printing = (** the integer is the number of real args, needed for reduction *) type case_info = - { ci_ind : inductive; - ci_npar : int; - 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 *) + { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) + ci_npar : int; (* number of parameters of the above inductive type *) + ci_cstr_ndecls : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (with let's) *) + ci_cstr_nargs : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (w/o let's) *) + ci_pp_info : case_printing (* not interpreted by the kernel *) } (** {6 The type of constructions } *) |