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

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 725859321..8b2402bb5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -135,6 +135,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;
 
@@ -223,6 +226,7 @@ let subst_mind_packet sub mbp =
     mind_arity = subst_arity sub mbp.mind_arity;
     mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
+    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
     mind_nb_constant = mbp.mind_nb_constant;