Types inductifs parametriques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 127 insertions, 87 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7877fbccb..cc59558e1 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -196,8 +196,9 @@ let rec str_const c =
       begin
 	match kind_of_term f with
 	| Construct((kn,j),i) -> 
-	    let oib = (lookup_mind kn !global_env).mind_packets.(j) in
-	    let num,arity = oib.mind_reloc_tbl.(i-1) in
+	    let oib = lookup_mind kn !global_env in
+	    let oip = oib.mind_packets.(j) in
+	    let num,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if nparams + arity = Array.length args then
 	    if arity = 0 then Bstrconst(Const_b0 num)
@@ -216,8 +217,9 @@ let rec str_const c =
       end
   | Ind ind -> Bstrconst (Const_ind ind)
   | Construct ((kn,j),i) ->  
-      let oib = (lookup_mind kn !global_env).mind_packets.(j) in
-      let num,arity = oib.mind_reloc_tbl.(i-1) in
+      let oib = lookup_mind kn !global_env in 
+      let oip = oib.mind_packets.(j) in
+      let num,arity = oip.mind_reloc_tbl.(i-1) in
       let nparams = oib.mind_nparams in
       if nparams + arity = 0 then Bstrconst(Const_b0 num)
       else Bconstruct_app(num,nparams,arity,[||])
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 72f37e226..9ce925207 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -80,8 +80,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
 type one_inductive_body = {
     mind_typename : identifier;
-    mind_nparams : int;
-    mind_params_ctxt : rel_context;
     mind_nrealargs : int;
     mind_nf_arity : types;
     mind_user_arity : types;
@@ -101,6 +99,9 @@ type mutual_inductive_body = {
     mind_finite : bool;
     mind_ntypes : int;
     mind_hyps : section_context;
+    mind_nparams : int;
+    mind_nparams_rec : int;
+    mind_params_ctxt : rel_context;
     mind_packets : one_inductive_body array;
     mind_constraints : constraints;
     mind_equiv : kernel_name option
@@ -128,9 +129,6 @@ let subst_mind_packet sub mbp =
     mind_sort = mbp.mind_sort;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_kelim = mbp.mind_kelim;
-    mind_nparams = mbp.mind_nparams;
-    mind_params_ctxt = 
-      map_rel_context (subst_mps sub) mbp.mind_params_ctxt;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
     mind_nb_constant = mbp.mind_nb_constant;
     mind_nb_args = mbp.mind_nb_args;
@@ -142,6 +140,10 @@ let subst_mind sub mib =
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+    mind_nparams = mib.mind_nparams;
+    mind_nparams_rec = mib.mind_nparams_rec;
+    mind_params_ctxt = 
+      map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints ;
     mind_equiv = option_app (subst_kn sub) mib.mind_equiv }
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3c99b67ac..62a1cc07c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -67,8 +67,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 type one_inductive_body = {
     mind_typename : identifier;
-    mind_nparams : int;
-    mind_params_ctxt : rel_context;
     mind_nrealargs : int;
     mind_nf_arity : types;
     mind_user_arity : types;
@@ -90,6 +88,9 @@ type mutual_inductive_body = {
     mind_finite : bool;
     mind_ntypes : int;
     mind_hyps : section_context;
+    mind_nparams : int;
+    mind_nparams_rec : int;
+    mind_params_ctxt : rel_context;
     mind_packets : one_inductive_body array;
     mind_constraints : constraints;
     mind_equiv : kernel_name option;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 6ea4bfc59..c31d8f74a 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -42,7 +42,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
 *)
 
 type one_inductive_entry = {
-  mind_entry_params : (identifier * local_entry) list;
   mind_entry_typename : identifier;
   mind_entry_arity : constr;
   mind_entry_consnames : identifier list;
@@ -51,6 +50,7 @@ type one_inductive_entry = {
 type mutual_inductive_entry = {
   mind_entry_record : bool;
   mind_entry_finite : bool;
+  mind_entry_params : (identifier * local_entry) list;
   mind_entry_inds : one_inductive_entry list }
 
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 71c756e26..6f4f343bb 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -42,7 +42,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
 *)
 
 type one_inductive_entry = {
-  mind_entry_params : (identifier * local_entry) list;
   mind_entry_typename : identifier;
   mind_entry_arity : constr;
   mind_entry_consnames : identifier list;
@@ -51,9 +50,9 @@ type one_inductive_entry = {
 type mutual_inductive_entry = {
   mind_entry_record : bool;
   mind_entry_finite : bool;
+  mind_entry_params : (identifier * local_entry) list;
   mind_entry_inds : one_inductive_entry list }
 
-
 (*s Constants (Definition/Axiom) *)
 
 type definition_entry = {
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6fac5c391..25464a3ce 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -187,16 +187,15 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   mind_check_arities env mie;
-  (* We first type params and arity of each inductive definition *)
+         (* Params are typed-checked here *)
+  let params = mie.mind_entry_params in
+  let env_params, params, cstp = infer_local_decls env params in
+  (* We first type arity of each inductive definition *)
   (* This allows to build the environment of arities and to share *)
   (* the set of constraints *)
   let cst, arities, rev_params_arity_list =
     List.fold_left
       (fun (cst,arities,l) ind ->
-         (* Params are typed-checked here *)
-	 let params = ind.mind_entry_params in
-	 let env_params, params, cst1 =
-           infer_local_decls env params in
          (* Arities (without params) are typed-checked here *)
 	 let arity, cst2 =
            infer_type env_params ind.mind_entry_arity in
@@ -206,10 +205,10 @@ let typecheck_inductive env mie =
 	    upper universe will be generated *)
 	 let id = ind.mind_entry_typename in
 	 let full_arity = it_mkProd_or_LetIn arity.utj_val params in
-	 Constraint.union cst (Constraint.union cst1 cst2),
+	 Constraint.union cst cst2,
 	 Sign.add_rel_decl (Name id, None, full_arity) arities,
          (params, id, full_arity, arity.utj_val)::l)
-      (Constraint.empty,empty_rel_context,[])
+      (cstp,empty_rel_context,[])
       mie.mind_entry_inds in
 
   let env_arities = push_rel_context arities env in
@@ -225,13 +224,13 @@ let typecheck_inductive env mie =
 	 let (issmall,isunit,lc',cst') =
 	   infer_constructor_packet env_arities params arsort lc in
 	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (params,id,full_arity,consnames,issmall,isunit,lc')
+	 let ind' = (id,full_arity,consnames,issmall,isunit,lc')
 	 in
 	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
       params_arity_list
       ([],cst) in
-  (env_arities, Array.of_list inds, cst)
+  (env_arities, params, Array.of_list inds, cst)
 
 (************************************************************************)
 (************************************************************************)
@@ -294,6 +293,26 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
 
+(* Computes the maximum number of recursive parameters : 
+    the first parameters which are constant in recursive arguments 
+    n is the current depth, nmr is the maximum number of possible 
+    recursive parameters *)
+
+let compute_rec_par (env,n,_,_) hyps nmr largs = 
+if nmr = 0 then 0 else
+(* start from 0, hyps will be in reverse order *)
+  let (lpar,_) = list_chop nmr largs in
+  let rec find k index = 
+      function 
+	  ([],_) -> nmr
+	| (_,[]) -> assert false (* |hyps|>=nmr *)
+	| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
+	| (p::lp,_::hyps) ->
+       ( match kind_of_term (whd_betadeltaiota env p) with
+	  | Rel w when w = index -> find (k+1) (index-1) (lp,hyps)
+          | _ -> k)
+  in find 0 (n-1) (lpar,List.rev hyps)
+
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
 let abstract_mind_lc env ntyps npars lc = 
@@ -327,13 +346,16 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   (* New index of the inductive types *)
   let newidx = n + auxntyp in
   (env', newidx, ntypes, ra_env')
+    
+let array_min nmr a = if nmr = 0 then 0 else
+  Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
 let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
   let nparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
-  let rec check_pos (env, n, ntypes, ra_env as ienv) c = 
+  let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = 
     let x,largs = decompose_app (whd_betadeltaiota env c) in
     match kind_of_term x with
       | Prod (na,b,d) ->
@@ -341,33 +363,34 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
 	  let b = whd_betadeltaiota env b in
           if not (noccur_between n ntypes b) then
 	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (ienv_push_var ienv (na, b, mk_norec)) d
+	  check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d
       | Rel k ->
-          let (ra,rarg) =
-            try List.nth ra_env (k-1)
-            with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in
-          (match ra with
-              Mrec _ -> check_correct_par ienv hyps (k-n+1) largs
-            | _ ->
-                if not (List.for_all (noccur_between n ntypes) largs)
-	        then raise (IllFormedInd (LocalNonPos n)));
-          rarg
+           (try let (ra,rarg) = List.nth ra_env (k-1) in 
+		let nmr1 =
+	       (match ra with
+                 Mrec _ -> compute_rec_par ienv hyps nmr largs
+		  |  _ -> nmr)
+		in 
+		  if not (List.for_all (noccur_between n ntypes) largs)
+	          then raise (IllFormedInd (LocalNonPos n))
+		  else (nmr1,rarg)
+            with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
       | Ind ind_kn ->
           (* If the inductive type being defined appears in a
              parameter, then we have an imbricated type *)
-          if List.for_all (noccur_between n ntypes) largs then mk_norec
-          else check_positive_imbr ienv (ind_kn, largs)
+          if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
+          else check_positive_imbr ienv nmr (ind_kn, largs)
       | err -> 
 	  if noccur_between n ntypes x &&
              List.for_all (noccur_between n ntypes) largs 
-	  then mk_norec
+	  then (nmr,mk_norec)
 	  else raise (IllFormedInd (LocalNonPos n))
 
   (* accesses to the environment are not factorised, but does it worth
      it? *)
-  and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) =
+  and check_positive_imbr (env,n,ntypes,ra_env as ienv) nmr (mi, largs) =
     let (mib,mip) = lookup_mind_specif env mi in
-    let auxnpar = mip.mind_nparams in
+    let auxnpar = mib.mind_nparams_rec in
     let (lpar,auxlargs) =
       try list_chop auxnpar largs 
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in 
@@ -385,31 +408,34 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
     let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
     (* Parameters expressed in env' *)
     let lpar' = List.map (lift auxntyp) lpar in
-    let irecargs = 
+    let irecargs_nmr = 
       (* fails if the inductive type occurs non positively *)
       (* when substituted *) 
       Array.map 
 	(function c -> 
 	  let c' = hnf_prod_applist env' c lpar' in 
-	  check_constructors ienv' false c') 
+	  check_constructors ienv' false nmr c') 
 	auxlcvect
+    in
+    let irecargs = Array.map snd irecargs_nmr
+    and nmr' = array_min nmr irecargs_nmr
     in 
-    (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)
+    (nmr,(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
   
   (* check the inductive types occur positively in the products of C, if
      check_head=true, also check the head corresponds to a constructor of
      the ith type *) 
 
-  and check_constructors ienv check_head c = 
-    let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = 
+  and check_constructors ienv check_head nmr c = 
+    let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = 
       let x,largs = decompose_app (whd_betadeltaiota env c) in
       match kind_of_term x with
 
         | Prod (na,b,d) -> 
 	    assert (largs = []);
-            let recarg = check_pos ienv b in 
+            let nmr',recarg = check_pos ienv nmr b in 
             let ienv' = ienv_push_var ienv (na,b,mk_norec) in
-	    check_constr_rec ienv' (recarg::lrec) d
+	    check_constr_rec ienv' nmr' (recarg::lrec) d
 
 	| hd ->
 	    if check_head then
@@ -420,32 +446,40 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
 	    else
 	      if not (List.for_all (noccur_between n ntypes) largs)
               then raise (IllFormedInd (LocalNonPos n));
-	    List.rev lrec
-    in check_constr_rec ienv [] c
+	    (nmr,List.rev lrec)
+    in check_constr_rec ienv nmr [] c
   in
-  mk_paths (Mrec i)
-    (Array.map
+  let irecargs_nmr =
+     Array.map
       (fun c ->
         let c = body_of_type c in
         let sign, rawc = mind_extract_params nparams c in
         let env' = push_rel_context sign env in
         try
-	  check_constructors ienv true rawc
+	  check_constructors ienv true nparams rawc
         with IllFormedInd err -> 
 	  explain_ind_err (ntypes-i) env nparams c err)
-      indlc)
+      indlc
+  in
+  let irecargs = Array.map snd irecargs_nmr
+  and nmr' = array_min nparams irecargs_nmr
+  in (nmr', mk_paths (Mrec i) irecargs)
 
-let check_positivity env_ar inds =
+let check_positivity env_ar params inds =
   let ntypes = Array.length inds in
   let lra_ind =
     List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
-  let check_one i (params,_,_,_,_,_,lc) =
-    let nparams = rel_context_length params in
+  let nparams = rel_context_length params in
+  let check_one i (_,_,_,_,_,lc) =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in
     let ienv = (env_ar, 1+nparams, ntypes, ra_env) in
-    check_positivity_one ienv params i lc in
-  Rtree.mk_rec (Array.mapi check_one inds)
+    check_positivity_one ienv params i lc 
+  in
+  let irecargs_nmr = Array.mapi check_one inds in 
+  let irecargs = Array.map snd irecargs_nmr
+  and nmr' = array_min nparams irecargs_nmr
+  in (nmr',Rtree.mk_rec irecargs)
 
 
 (************************************************************************)
@@ -476,12 +510,12 @@ let allowed_sorts env issmall isunit = function
       if isunit then all_sorts
       else logical_sorts
 
-let build_inductive env env_ar record finite inds recargs cst =
+let build_inductive env env_ar params record finite inds nmr recargs cst =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
     Array.fold_left 
-      (fun acc (_,_,ar,_,_,_,lc) -> 
+      (fun acc (_,ar,_,_,_,lc) -> 
 	 Idset.union (Environ.global_vars_set env (body_of_type ar))
 	   (Array.fold_left
 	      (fun acc c ->
@@ -490,10 +524,10 @@ let build_inductive env env_ar record finite inds recargs cst =
 	      lc))
       Idset.empty inds in
   let hyps = keep_hyps env ids in
+  let nparamargs = rel_context_nhyps params in
   (* Check one inductive *)
-  let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg =
+  let build_one_packet (id,ar,cnames,issmall,isunit,lc) recarg =
     (* Arity in normal form *)
-    let nparamargs = rel_context_nhyps params in
     let (ar_sign,ar_sort) = dest_arity env ar in
     let nf_ar =
       if isArity (body_of_type ar) then ar
@@ -521,8 +555,6 @@ let build_inductive env env_ar record finite inds recargs cst =
     let rtbl = Array.init (List.length cnames) transf in
     (* Build the inductive packet *)
     { mind_typename = id;
-      mind_nparams = nparamargs;
-      mind_params_ctxt = params;
       mind_user_arity  = ar;
       mind_nf_arity = nf_ar;
       mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
@@ -542,6 +574,9 @@ let build_inductive env env_ar record finite inds recargs cst =
     mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
+    mind_nparams = nparamargs;
+    mind_nparams_rec = nmr;  
+    mind_params_ctxt = params;
     mind_packets = packets;
     mind_constraints = cst;
     mind_equiv = None;
@@ -552,10 +587,11 @@ let build_inductive env env_ar record finite inds recargs cst =
 
 let check_inductive env mie =
   (* First type-check the inductive definition *)
-  let (env_arities, inds, cst) = typecheck_inductive env mie in
+  let (env_ar, params, inds, cst) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let recargs = check_positivity env_arities inds in
+  let (nmr,recargs) = check_positivity env_ar params inds in
   (* Build the inductive packets *)
-  build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite 
-    inds recargs cst
+  build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite 
+    inds nmr recargs cst
+
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3b152aae..bf64dfda0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -80,13 +80,13 @@ let instantiate_params t args sign =
   if rem_args <> [] then fail();
   type_app (substl subs) ty
 
-let full_inductive_instantiate mip params t =
-  instantiate_params t params mip.mind_params_ctxt
+let full_inductive_instantiate mib params t =
+  instantiate_params t params mib.mind_params_ctxt
 
-let full_constructor_instantiate (((mind,_),mib,mip),params) =
+let full_constructor_instantiate (((mind,_),mib,_),params) =
   let inst_ind = constructor_instantiate mind mib in
   (fun t ->
-    instantiate_params (inst_ind t) params mip.mind_params_ctxt)
+    instantiate_params (inst_ind t) params mib.mind_params_ctxt)
 
 (************************************************************************)
 (************************************************************************)
@@ -148,12 +148,12 @@ let local_rels ctxt =
   rels
 
 (* Get type of inductive, with parameters instantiated *)
-let get_arity mip params =
+let get_arity mib mip params =
   let arity = mip.mind_nf_arity in
-  destArity (full_inductive_instantiate mip params arity)
+  destArity (full_inductive_instantiate mib params arity)
 
-let build_dependent_inductive ind mip params =
-  let arsign,_ = get_arity mip params in
+let build_dependent_inductive ind mib mip params =
+  let arsign,_ = get_arity mib mip params in
   let nrealargs = mip.mind_nrealargs in
   applist 
     (mkInd ind, (List.map (lift nrealargs) params)@(local_rels arsign))
@@ -162,9 +162,9 @@ let build_dependent_inductive ind mip params =
 (* This exception is local *)
 exception LocalArity of (constr * constr * arity_error) option
 
-let is_correct_arity env c pj ind mip params = 
+let is_correct_arity env c pj ind mib mip params = 
   let kelim = mip.mind_kelim in
-  let arsign,s = get_arity mip params in
+  let arsign,s = get_arity mib mip params in
   let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
   let rec srec env pt t u =
     let pt' = whd_betadeltaiota env pt in
@@ -180,7 +180,7 @@ let is_correct_arity env c pj ind mip params =
           let ksort = match kind_of_term k with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (LocalArity None) in
-	  let dep_ind = build_dependent_inductive ind mip params in
+	  let dep_ind = build_dependent_inductive ind mib mip params in
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
@@ -224,7 +224,7 @@ let build_branches_type ind mib mip params dep p =
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop mip.mind_nparams allargs in
+    let (lparams,vargs) = list_chop mib.mind_nparams allargs in
     let cargs =
       if dep then
         let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -244,10 +244,10 @@ let build_case_type dep p c realargs =
 
 let type_case_branches env (ind,largs) pj c =
   let (mib,mip) = lookup_mind_specif env ind in 
-  let nparams = mip.mind_nparams in
+  let nparams = mib.mind_nparams in
   let (params,realargs) = list_chop nparams largs in
   let p = pj.uj_val in
-  let (dep,univ) = is_correct_arity env c pj ind mip params in
+  let (dep,univ) = is_correct_arity env c pj ind mib mip params in
   let lc = build_branches_type ind mib mip params dep p in
   let ty = build_case_type dep p c realargs in
   (lc, ty, univ)
@@ -270,7 +270,7 @@ let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
     (indsp <> ci.ci_ind) or
-    (mip.mind_nparams <> ci.ci_npar)
+    (mib.mind_nparams <> ci.ci_npar)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
@@ -770,7 +770,7 @@ let check_one_cofix env nbfix def deftype =
             let lra =vlra.(i-1) in 
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
-            let realargs = list_skipn mip.mind_nparams args in
+            let realargs = list_skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) -> 
                   if rar = mk_norec then
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 033eeec79..f87dc90e4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -114,8 +114,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 	    && Array.length mib2.mind_packets >= 1);
 
        (* TODO: we should allow renaming of parameters at least ! *)
-  check (fun mib -> mib.mind_packets.(0).mind_nparams);
-  check (fun mib -> mib.mind_packets.(0).mind_params_ctxt); 
+  check (fun mib -> mib.mind_nparams);
+  check (fun mib -> mib.mind_params_ctxt); 
 
   begin 
     match mib2.mind_equiv with
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 5ef84adc7..cdc9fa0f7 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -318,7 +318,7 @@ let find_rectype typ =
 let construct_of_constr_block env tag typ =
   let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let nparams = mip.mind_nparams in
+  let nparams = mib.mind_nparams in
   let rtbl = mip.mind_reloc_tbl in
   let i = invert_tag false tag rtbl in
   let params = Array.sub allargs 0 nparams in
@@ -429,7 +429,7 @@ and nf_stk env c t stk  =
   | Zswitch sw :: stk -> 
       let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
-      let nparams = mip.mind_nparams in
+      let nparams = mib.mind_nparams in
       let params,realargs = Util.array_chop nparams allargs in
       (* calcul du predicat du case, 
         [dep] indique si c'est un case dependant *)