From a07e31a2693bde01d3dca59364693096d550561a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Aug 2009 15:15:46 +0000
Subject: 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
---
 kernel/declarations.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 725859321c..8b2402bb54 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;
-- 
cgit v1.2.3