diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 10:07:53 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:57 +0100 |
| commit | b88929d9d8de179a7e356cf9cbe2afef76f905a3 (patch) | |
| tree | 66cb060ce8034e56cf5360e206f8cf2593204ef1 /kernel/constr.mli | |
| parent | 1b5f85d38db7a0d7cb9a4b9491a5563461373182 (diff) | |
COMMENTS: added to the "Constr.case_info" type.
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 14 |
1 files changed, 9 insertions, 5 deletions
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 } *) |