COMMENTS: added to the "Constr.case_info" type.

1 files changed, 9 insertions, 5 deletions

diff --git a/kernel/constr.mli b/kernel/constr.mli
index 70f1699314..edd4eb2310 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 } *)