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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.ml | 9 +++++---- kernel/inductive.ml | 4 ++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/kernel/closure.ml b/kernel/closure.ml index b64f6fe59..08b0cd065 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) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d319f633a..493cb15f5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -23,7 +23,7 @@ let build_mis ((sp,tyi),args) mib = mis_mip = mind_nth_type_packet mib tyi } let mis_ntypes mis = mis.mis_mib.mind_ntypes -let mis_nparams mis = mis.mis_mib.mind_nparams +let mis_nparams mis = mis.mis_mip.mind_nparams let mis_index mis = mis.mis_tyi @@ -97,7 +97,7 @@ let mis_nf_arity mis = let mis_params_ctxt mispec = let paramsign,_ = - decompose_prod_n_assum mispec.mis_mib.mind_nparams + decompose_prod_n_assum mispec.mis_mip.mind_nparams (body_of_type (mis_nf_arity mispec)) in paramsign -- cgit v1.2.3