From ed20a4e9c320ae4bb2f724d181fbb351079d00b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Dec 2000 22:18:47 +0000
Subject: Les params d'inductif deviennent en même temps propre à chaque
 inductif d'un bloc et en même temps factorisés dans l'arité et les
 constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour
 mutual_inductive_body); accessoirement cela permet de factoriser le calcul
 des univers des paramètres dans safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index b64f6fe593..08b0cd0654 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -491,8 +491,9 @@ let cofixp_reducible redfun flgs _ stk =
   else 
     false
 
-let mindsp_nparams env sp =
-  let mib = lookup_mind sp env in mib.Declarations.mind_nparams
+let mindsp_nparams env (sp,i) =
+  let mib = lookup_mind sp env in
+  (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams
 
 (* The main recursive functions
  *
@@ -615,7 +616,7 @@ and cbv_stack_term info stack env t =
 
     (* constructor in a Case -> IOTA
        (use red_under because we know there is a Case) *)
-    | (CONSTR(n,(sp,_),_,_), APP(args,CASE(_,br,_,env,stk)))
+    | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,_,env,stk)))
             when red_under info.i_flags IOTA ->
               let nparams = mindsp_nparams info.i_env sp in
               let real_args = snd (list_chop nparams args) in
@@ -1046,7 +1047,7 @@ type case_status =
 let constr_or_cofix env v =
   let (lft_hd, head, appl) = strip_freeze v in
   match head.term with
-    | FConstruct (((indsp,_),i),_) ->
+    | FConstruct ((indsp,i),_) ->
         let args = snd (array_chop (mindsp_nparams env indsp) appl) in
         CONSTRUCTOR (i, args)
     | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env)
-- 
cgit v1.2.3