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 | |
parent | 1b5f85d38db7a0d7cb9a4b9491a5563461373182 (diff) |
COMMENTS: added to the "Constr.case_info" type.
Diffstat (limited to 'kernel')
-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 } *) |