COMMENTS: of "Constr.case_info" type were updated.

1 files changed, 13 insertions, 7 deletions

diff --git a/kernel/constr.mli b/kernel/constr.mli
index edd4eb231..ada268606 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -30,16 +30,22 @@ type case_printing =
     cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
     style     : case_style }
 
-(** the integer is the number of real args, needed for reduction *)
+(* INVARIANT:
+ * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs
+ * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)),
+ *          ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i)
+ *)
 type case_info =
   { 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_cstr_ndecls : int array;     (* For each constructor, the corresponding integer determines
+                                       the number of values that can be bound in a match-construct.
+                                       NOTE: parameters of the inductive type are therefore excluded from the count *)
+    ci_cstr_nargs : int array;      (* for each constructor, the corresponding integers determines
+                                       the number of values that can be applied to the constructor,
+                                       in addition to the parameters of the related inductive type
+                                       NOTE: "lets" are therefore excluded from the count
+                                       NOTE: parameters of the inductive type are also excluded from the count *)
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }