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/indtypes.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4aac096fc4..ccf9b3f6c5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -588,6 +588,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
   (* Compute the set of used section variables *)
   let hyps =  used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
+  let nparamdecls = rel_context_length params in
   (* Check one inductive *)
   let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
@@ -629,6 +630,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_arity = arkind;
 	mind_arity_ctxt = ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
+	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealargs;
-- 
cgit v1.2.3