Transfers to checker ("let"s in inductive arities + Coq root read-only).

- Support for let's in the signature of the arity of an inductive type was
  in the kernel part of commit 12273,
- Support for binding Coq root read-only in -R option was in commit 12220.

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

1 files changed, 1 insertions, 1 deletions

diff --git a/checker/term.ml b/checker/term.ml
index f245d15518..f5b2496c85 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -28,7 +28,7 @@ type metavariable = int
 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;