Ensures that let-in's in arities of inductive types work well. Maybe not

very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index da8a77883..8a2c3278c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -26,7 +26,7 @@ type metavariable = int
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;