From b88929d9d8de179a7e356cf9cbe2afef76f905a3 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 18 Dec 2015 10:07:53 +0100 Subject: COMMENTS: added to the "Constr.case_info" type. --- kernel/constr.mli | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'kernel/constr.mli') 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 } *) -- cgit v1.2.3