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, 3 insertions, 0 deletions

diff --git a/checker/declarations.mli b/checker/declarations.mli
index b376151ca..c5b676bda 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -86,6 +86,9 @@ type one_inductive_body = {
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
+ (* Length of realargs context (with let, no params) *)
+    mind_nrealargs_ctxt : int;
+
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;