From cb8db3f7af710970a4ddba2fc559910ff7feaffb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 6 Sep 2003 14:17:55 +0000
Subject: Mise en place possibilité de définitions locales dans les paramètres
 des inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml     |  2 +-
 pretyping/inductiveops.ml | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 01b1bc824f..49034b1b1f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -202,7 +202,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
   let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in
   let get_consnarg j = 
     let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in
-    let _,t = decompose_prod_n_assum mip.mind_nparams typi in
+    let _,t = decompose_prod_n_assum (List.length mip.mind_params_ctxt) typi in
     List.rev (fst (decompose_prod_assum t)) in
   let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
   let consnargsl = Array.map List.length consnargs in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adc5932f18..792fe6d2d9 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -150,10 +150,16 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
+let rec instantiate args c = match kind_of_term c, args with
+  | Prod (_,_,c), a::args -> instantiate args (subst1 a c)
+  | LetIn (_,b,_,c), args -> instantiate args (subst1 b c)
+  | _, [] -> c
+  | _ -> anomaly "too short arity"
+
 let get_arity env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let arity = body_of_type mip.mind_nf_arity in
-  destArity (prod_applist arity params)
+  let arity = mip.mind_nf_arity in
+  destArity (instantiate params arity)
 
 (* Functions to build standard types related to inductive *)
 let build_dependent_constructor cs =
-- 
cgit v1.2.3