Types inductifs parametriques

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

36 files changed, 296 insertions, 194 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d685051e9..71545d966 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -58,7 +58,7 @@ let rec decompose_term env t=
 	let targs=Array.map (decompose_term env) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Construct c->
-	let (_,oib)=Global.lookup_inductive (fst c) in
+	let (oib,_)=Global.lookup_inductive (fst c) in
 	let nargs=mis_constructor_nargs_env env c in
 	  Constructor {ci_constr=c;
 		       ci_arity=nargs;
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0eb35e95b..55ad52ee2 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in 
-    let npar = mip0.mind_nparams in
-    let epar = push_rel_context mip0.mind_params_ctxt env in
+    let npar = mib.mind_nparams in
+    let epar = push_rel_context mib.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets = 
@@ -358,7 +358,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in 
 	let field_names = 
-	  list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
+	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in 
 	let mp,d,_ = repr_kn kn in 
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 9dbda969a..4e256981f 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -47,7 +47,7 @@ let rec nb_prod_after n c=
 
 let construct_nhyps ind gls =
   let env=pf_env gls in
-  let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
   let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
     Array.map hyp constr_types
@@ -99,7 +99,7 @@ let rec kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mip.mind_nparams in  
+			    nb_prod c = mib.mind_nparams in  
 			    array_exists is_constant mip.mind_nf_lc in 
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5b265ec86..2560b0b82 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1556,7 +1556,7 @@ and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let p = mip.mind_nparams in
+  let p = mib.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
   let lp=ref (get_constructors env indf).(c).cs_args in
   let lr=ref [] in
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index df059677b..e8f149402 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -38,6 +38,8 @@ let print_if_verbose s = if !verbose then print_string s;;
 (* Next exception is used only inside print_coq_object and tag_of_string_tag *)
 exception Uninteresting;;
 
+(* NOT USED anymore, we back to the V6 point of view with global parameters 
+
 (* Internally, for Coq V7, params of inductive types are associated     *)
 (* not to the whole block of mutual inductive (as it was in V6) but to  *)
 (* each member of the block; but externally, all params are required    *)
@@ -60,6 +62,8 @@ let extract_nparams pack =
   done;
   nparams0
 
+*)
+
 (* could_have_namesakes sp = true iff o is an object that could be cooked and *)
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
@@ -392,11 +396,11 @@ let mk_constant_obj id bo ty variables hyps =
          ty,params)
 ;;
 
-let mk_inductive_obj sp packs variables hyps finite =
+let mk_inductive_obj sp packs variables nparams hyps finite =
  let module D = Declarations in
   let hyps = string_list_of_named_context_list hyps in
   let params = filter_params variables hyps in
-  let nparams = extract_nparams packs in
+(*  let nparams = extract_nparams packs in *)
    let tys =
     let tyno = ref (Array.length packs) in
     Array.fold_right
@@ -524,10 +528,11 @@ let print internal glob_ref kind xml_library_root =
         G.lookup_constant kn in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
-       let {D.mind_packets=packs ;
+       let {D.mind_nparams=nparams;
+	    D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
-          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables hyps finite
+          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
diff --git a/ide/coq.ml b/ide/coq.ml
index 0a72c97bc..eeb31e1ae 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -432,10 +432,8 @@ let make_cases s =
   let glob_ref = Nametab.locate qualified_name in
   match glob_ref with
     | Libnames.IndRef i -> 
-	let _,
-	{
-	  Declarations.mind_nparams = np ;
-	  Declarations.mind_consnames = carr ;
+	let {Declarations.mind_nparams = np},
+	{Declarations.mind_consnames = carr ;
 	 Declarations.mind_nf_lc = tarr } 
 	= Global.lookup_inductive i 
 	in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a5b022058..8faec21df 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1254,7 +1254,7 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | a, AHole _ when not(Options.do_translate()) -> sigma
   | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
       let nparams =
-	(snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let l2 =
         match a2 with
 	  | ARef (ConstructRef r2) when r1 = r2 -> []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b2b657c5f..498c483dc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -462,7 +462,7 @@ let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
   | ARef (ConstructRef c) ->
       (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)])
   | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
-      let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let _,args = list_chop nparams args in
       let idslpll = List.map (aux ([],[]) subst) args in
       let ids',pll = product_of_cases_patterns ids idslpll in
@@ -500,7 +500,7 @@ let rec patt_of_rawterm loc cstr =
     | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
     | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
         if !dump then add_glob loc x;
-        let (_,mib) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
+        let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
         let npar = mib.Declarations.mind_nparams in
         let (params,args) =
           if List.length pl <= npar then (pl,[]) else
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 *)
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 80523d588..554af8163 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -9,7 +9,8 @@
 (*i $Id$ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
-type 'a t
+
+type 'a t 
 
 (* Building trees *)
 (* build a recursive call *) 
diff --git a/library/declare.ml b/library/declare.ml
index 6bace2654..1b48acf04 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -43,9 +43,9 @@ let string_of_strength = function
   | Global -> "(global)"
 
 (* XML output hooks *)
-let xml_declare_variable = ref (fun sp -> ())
-let xml_declare_constant = ref (fun sp -> ())
-let xml_declare_inductive = ref (fun sp -> ())
+let xml_declare_variable = ref (fun (sp:object_name) -> ())
+let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
 
 let if_xml f x = if !Options.xml_export then f x else ()
 
@@ -291,7 +291,6 @@ let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
         Discharge.process_inductive sechyps repl mie)
 
 let dummy_one_inductive_entry mie = {
-  mind_entry_params = [];
   mind_entry_typename = mie.mind_entry_typename;
   mind_entry_arity = mkProp;
   mind_entry_consnames = mie.mind_entry_consnames;
@@ -300,6 +299,7 @@ let dummy_one_inductive_entry mie = {
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_inductive_entry (_,imps,m) = ([],imps,{
+  mind_entry_params = [];
   mind_entry_record = false;
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
diff --git a/library/library.ml b/library/library.ml
index ce4fa533c..456658760 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -308,7 +308,8 @@ let (in_import, out_import) =
 (*s Loading from disk to cache (preparation phase) *)
 
 let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
-let vo_magic_number8 = 08002 (* V8.0 final new syntax *)
+(* let vo_magic_number8 = 08002 (* V8.0 final new syntax *) *)
+let vo_magic_number8 = 08003 (* V8.0 final new syntax + new params in ind *)
 
 let (raw_extern_library7, raw_intern_library7) =
   System.raw_extern_intern vo_magic_number7 ".vo"
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index ac5c7430f..97139ec15 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -285,7 +285,7 @@ let print_constructors envpar names types =
 
 let build_inductive sp tyi =
   let (mib,mip) = Global.lookup_inductive (sp,tyi) in
-  let params = mip.mind_params_ctxt in
+  let params = mib.mind_params_ctxt in
   let args = extended_rel_list 0 params in
   let env = Global.env() in
   let arity = hnf_prod_applist env mip.mind_user_arity args in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 536317613..8b6e476c7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -219,7 +219,7 @@ let detype_case computable detype detype_eqn testdep
   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 (List.length mip.mind_params_ctxt) typi in
+    let _,t = decompose_prod_n_assum (List.length mib.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
@@ -253,7 +253,7 @@ let detype_case computable detype detype_eqn testdep
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
 	      else 
-		let pars = list_tabulate (fun _ -> Anonymous) mip.mind_nparams
+		let pars = list_tabulate (fun _ -> Anonymous) mib.mind_nparams
 		in Some (dummy_loc,indsp,pars@nl) in
             n, aliastyp, Some typ, Some p
   in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e6d674a5e..e58609195 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -41,7 +41,7 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
    lifter les paramètres globaux *)
 
 let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
-  let lnamespar = mip.mind_params_ctxt in
+  let lnamespar = mib.mind_params_ctxt in
   let dep = match depopt with 
     | None -> mip.mind_sort <> (Prop Null)
     | Some d -> d
@@ -191,7 +191,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
   let c = it_mkProd_or_LetIn base cs.cs_args in
   process_constr env 0 c recargs nhyps []
 
-let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = 
+let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = 
   let process_pos env fk  =
     let rec prec env i hyps p =
       let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
@@ -203,7 +203,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ -> 
-            let realargs = list_skipn nparams largs
+            let realargs = list_skipn nparrec largs
             and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in 
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
@@ -245,9 +245,12 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
 (* Main function *)
-let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
-  let nparams = mip.mind_nparams in
-  let lnamespar = mip.mind_params_ctxt in
+let mis_make_indrec env sigma listdepkind mib =
+  let nparams = mib.mind_nparams in
+  let nparrec = mib. mind_nparams_rec in
+  let lnamespar = mib.mind_params_ctxt in
+  let lnonparrec,lnamesparrec = 
+    list_chop (nparams-nparrec) mib.mind_params_ctxt in
   let nrec = List.length listdepkind in
   let depPvec =
     Array.create mib.mind_ntypes (None : (bool * constr) option) in 
@@ -262,6 +265,11 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
     assign nrec listdepkind in 
   let recargsvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
+ (* recarg information for non recursive parameters *)
+  let rec recargparn l n = 
+    if n = 0 then l else recargparn (mk_norec::l) (n-1) 
+  in
+  let recargpar = recargparn [] (nparams-nparrec) in
   let make_one_rec p =
     let makefix nbconstruct =
       let rec mrec i ln ltyp ldef = function
@@ -272,59 +280,86 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 
             (* arity in the context of the fixpoint, i.e.
                 P1..P_nrec f1..f_nbconstruct *)
-	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
+	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
 
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
-
+	    
+	    let nonrecpar = nparams-nparrec in
 	    let nar = mipi.mind_nrealargs in
 	    let ndepar = nar + 1 in
-	    let dect = ndepar+nrec+nbconstruct in
+	    let dect = nonrecpar+ndepar+nrec+nbconstruct in
 
-	    let branches = 
               (* constructors in context of the Cases expr, i.e.
-                 P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
-	      let args' = extended_rel_list (dect+nrec) lnamespar in
-              let indf' = make_ind_family(indi,args') in
+         P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
+	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
+	    let args'' = extended_rel_list ndepar lnonparrec in
+            let indf' = make_ind_family(indi,args'@args'') in
+
+	    let branches = 
 	      let constrs = get_constructors env indf' in
-	      let vecfi = rel_vect (dect-i-nctyi) nctyi in
+	      let fi = rel_vect (dect-i-nctyi) nctyi in
+	      let vecfi = Array.map 
+			    (fun f -> appvect (f,rel_vect ndepar nonrecpar))
+			    fi 
+	      in
 	      array_map3
-		(make_rec_branch_arg env sigma (nparams,depPvec,ndepar))
-                vecfi constrs (dest_subterms recargsvec.(tyi)) in
+		(make_rec_branch_arg env sigma 
+		   (nparrec,depPvec,ndepar+nonrecpar))
+                vecfi constrs (dest_subterms recargsvec.(tyi)) 
+	    in
 
 	    let j = (match depPvec.(tyi) with 
 		       | Some (_,c) when isRel c -> destRel c 
-		       | _ -> assert false) in
+		       | _ -> assert false) 
+	    in
+
+	      (* Predicate in the context of the case *)
+
+	    let depind' = build_dependent_inductive env indf' in
+	    let arsign',_ = get_arity env indf' in
+	    let deparsign' = (Anonymous,None,depind')::arsign' in
+
 	    let pargs =
-	      if dep then extended_rel_vect 0 deparsign
-	      else extended_rel_vect 1 arsign in
-	    let concl = appvect (mkRel (nbconstruct+ndepar+j),pargs) in
+	      let nrpar = extended_rel_list (2*ndepar) lnonparrec 
+	      and nrar = if dep then extended_rel_list 0 deparsign'
+	      else extended_rel_list 1 arsign'
+	      in nrpar@nrar
+
+	    in
 
 	    (* body of i-th component of the mutual fixpoint *)
 	    let deftyi = 
 	      let ci = make_default_case_info env RegularStyle indi in
-	      let p =
+	      let concl = applist (mkRel (dect+j+ndepar),pargs) in 
+	      let pred =
 		it_mkLambda_or_LetIn_name env 
 		  ((if dep then mkLambda_name env else mkLambda)
-		   (Anonymous,depind,concl))
-		  arsign
+		   (Anonymous,depind',concl))
+		  arsign'
 	      in
 	      it_mkLambda_or_LetIn_name env
-		(mkCase (ci, lift (nrec+ndepar) p, 
+		(mkCase (ci, pred, 
 		             mkRel 1,
 			     branches))
 		(lift_rel_context nrec deparsign)
 	    in
 
 	    (* type of i-th component of the mutual fixpoint *)
+
 	    let typtyi =
-	      it_mkProd_or_LetIn_name env
+	    let concl = 
+	      let pargs = if dep then extended_rel_vect 0 deparsign
+	      else extended_rel_vect 1 arsign
+	      in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
+	    in it_mkProd_or_LetIn_name env
 		concl
 		deparsign
 	    in
-	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest
+	    mrec (i+nctyi) (nar+nonrecpar::ln) (typtyi::ltyp) 
+                 (deftyi::ldef) rest
         | [] -> 
 	    let fixn = Array.of_list (List.rev ln) in
             let fixtyi = Array.of_list (List.rev ltyp) in
@@ -343,7 +378,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	      make_branch env (i+j) rest 
 	    else 
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
-	      let vargs = extended_rel_list (nrec+i+j) lnamespar in
+	      let recarg = recargpar@recarg in
+	      let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
 	      let indf = (indi, vargs) in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
 	      let p_0 =
@@ -358,7 +394,7 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
     in 
     let rec put_arity env i = function 
       | (indi,_,_,dep,kinds)::rest -> 
-	  let indf = make_ind_family (indi,extended_rel_list i lnamespar) in
+	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
 	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
 	  mkLambda_string "P" typP
 	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
@@ -366,12 +402,14 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	  make_branch env 0 listdepkind 
     in 
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-    let env' = push_rel_context lnamespar env in
+
     if mis_is_recursive_subset
       (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
       mipi.mind_recargs
     then 
-      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar
+    let env' = push_rel_context lnamesparrec env in
+      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
+	lnamesparrec
     else 
       mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind 
   in 
@@ -437,16 +475,22 @@ let instanciate_type_indrec_scheme sort npars term =
 
 (**********************************************************************)
 (* Interface to build complex Scheme *)
+(* Check inductive types only occurs once 
+(otherwise we obtain a meaning less scheme) *)
 
 let check_arities listdepkind = 
-  List.iter 
-    (function (indi,mibi,mipi,dep,kind) -> 
+  let _ = List.fold_left
+    (fun ln ((_,ni),mibi,mipi,dep,kind) -> 
        let id = mipi.mind_typename  in
        let kelim = mipi.mind_kelim in
        if not (List.exists ((=) kind) kelim) then
 	 raise
-	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
-    listdepkind
+	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind)))
+       else if List.mem ni ln then raise
+	   (InductiveError NotMutualInScheme)
+       else ni::ln)
+	    [] listdepkind
+  in true
 
 let build_mutual_indrec env sigma = function 
   | (mind,mib,mip,dep,s)::lrecspec ->
@@ -464,14 +508,14 @@ let build_mutual_indrec env sigma = function
 	   lrecspec)
       in
       let _ = check_arities listdepkind in 
-      mis_make_indrec env sigma listdepkind (mind,mib,mip)
+      mis_make_indrec env sigma listdepkind mib
   | _ -> anomaly "build_indrec expects a non empty list of inductive types"
 
 let build_indrec env sigma ind =
   let (mib,mip) = lookup_mind_specif env ind in
   let kind = family_of_sort mip.mind_sort in
   let dep = kind <> InProp in
-  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] (ind,mib,mip))
+  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (**********************************************************************)
 (* To handle old Case/Match syntax in Pretyping                       *)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index d96908a7b..2306201b2 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -54,3 +54,6 @@ val make_rec_branch_arg :
 val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier
+
+
+
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a0b2cb80f..c540a4a1f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -105,7 +105,7 @@ let mis_constr_nargs_env env (kn,i) =
 let mis_constructor_nargs_env env ((kn,i),j) =
   let mib = Environ.lookup_mind kn env in
   let mip = mib.mind_packets.(i) in 
-  recarg_length mip.mind_recargs j + mip.mind_nparams
+  recarg_length mip.mind_recargs j + mib.mind_nparams
 
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
@@ -115,7 +115,7 @@ let make_case_info env ind style pats_source =
       style     = style;
       source    = pats_source } in
   { ci_ind     = ind;
-    ci_npar    = mip.mind_nparams;
+    ci_npar    = mib.mind_nparams;
     ci_pp_info = print_info }
 
 let make_default_case_info env style ind =
@@ -140,6 +140,7 @@ let lift_constructor n cs = {
   cs_args = lift_rel_context n cs.cs_args;
   cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
 }
+(* Accept less parameters than in the signature *)
 
 let instantiate_params t args sign =
   let rec inst s t = function
@@ -151,17 +152,17 @@ let instantiate_params t args sign =
 	(match kind_of_term t with
 	   | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
 	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
-    | [], [] -> substl s t
+    | _, [] -> substl s t
     | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
   in inst [] t (List.rev sign,args)
 
 let get_constructor (ind,mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (ind,mib,mip) j in
-  let typi = instantiate_params typi params mip.mind_params_ctxt in
+  let typi = instantiate_params typi params mib.mind_params_ctxt in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
-  let vargs = list_skipn mip.mind_nparams allargs in
+  let vargs = list_skipn (List.length params) allargs in
   { cs_cstr = ith_constructor_of_inductive ind j;
     cs_params = params;
     cs_nargs = rel_context_length args;
@@ -194,7 +195,7 @@ let build_dependent_constructor cs =
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let nrealargs = mip.mind_nrealargs in
+  let nrealargs = List.length arsign in
   applist 
     (mkInd ind,
      (List.map (lift nrealargs) params)@(extended_rel_list 0 arsign))
@@ -243,7 +244,7 @@ let find_rectype env sigma c =
   match kind_of_term t with
     | Ind ind ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
-        let (par,rargs) = list_chop mip.mind_nparams l in
+        let (par,rargs) = list_chop mib.mind_nparams l in
         IndType((ind, par),rargs)
     | _ -> raise Not_found
 
@@ -313,12 +314,12 @@ let set_names env n brty =
   it_mkProd_or_LetIn_name env cl ctxt
 
 let set_pattern_names env ind brv =
-  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
       (fun c ->
         rel_context_length (fst (decompose_prod_assum c)) -
-        mip.mind_nparams)
+        mib.mind_nparams)
       mip.mind_nf_lc in
   array_map2 (set_names env) arities brv
 
@@ -327,7 +328,7 @@ let type_case_branches_with_names env indspec pj c =
   let (ind,args) = indspec in
   let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let params = list_firstn mip.mind_nparams args in
+  let params = list_firstn mib.mind_nparams args in
   if is_elim_predicate_explicitly_dependent env pj.uj_val (ind,params) then
     (set_pattern_names env ind lbrty, conclty)
   else (lbrty, conclty)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b5d6318dc..497739692 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -101,7 +101,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
     (* build now the fixpoint *)
     let lnames,_ = get_arity env indf in
     let nar = List.length lnames in
-    let nparams = mip.mind_nparams in
+    let nparams = mib.mind_nparams in
     let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
     let branches = 
       array_map3
@@ -893,7 +893,7 @@ let rec pretype tycon env isevars lvar = function
             let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
             let get_consnarg j = 
               let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in
-              let _,t = decompose_prod_n_assum mip.mind_nparams typi in
+              let _,t = decompose_prod_n_assum mib.mind_nparams 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/recordops.ml b/pretyping/recordops.ml
index 4157b383c..b3180b06b 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -42,7 +42,7 @@ let projection_table = ref Cmap.empty
 let option_fold_right f p e = match p with Some a -> f a e | None -> e
 
 let load_structure i (_,(ind,id,kl,projs)) =
-  let n = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
   let struc =
     { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 770f2d6b7..9d19d37e8 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -127,7 +127,7 @@ let solveLeftBranch rectype g =
   try
     let (lhs,rhs) = match_eqdec_partial (pf_concl g) in
     let (mib,mip) = Global.lookup_inductive rectype in
-    let nparams   = mip.mind_nparams in
+    let nparams   = mib.mind_nparams in
     let getargs l = list_skipn nparams (snd (decompose_app l)) in
     let rargs   = getargs rhs
     and largs   = getargs lhs in 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ef96e5fe..4797146a3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -393,7 +393,7 @@ let rec build_discriminator sigma env dirn c sort = function
       let (ind,_) = dest_ind_family indf in
       let (mib,mip) = lookup_mind_specif env ind in
       let _,arsort = get_arity env indf in
-      let nparams = mip.mind_nparams  in
+      let nparams = mib.mind_nparams  in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
@@ -673,7 +673,7 @@ let rec build_injrec sigma env dflt c = function
       let cty = type_of env sigma c in
       let (ity,_) = find_mrectype env sigma cty in
       let (mib,mip) = lookup_mind_specif env ity in
-      let nparams = mip.mind_nparams in
+      let nparams = mib.mind_nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let (subval,tuplety,dfltval) =
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index dfdacbb99..c3735b2c8 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -120,7 +120,7 @@ let match_with_unit_type t =
         let constr_types = mip.mind_nf_lc in 
         let nconstr = Array.length mip.mind_consnames in
         let zero_args c =
-          nb_prod c = mip.mind_nparams in  
+          nb_prod c = mib.mind_nparams in  
 	if nconstr = 1 && array_for_all zero_args constr_types then 
 	  Some hdapp
         else 
@@ -213,11 +213,11 @@ let match_with_nodep_ind t =
       | Ind ind  -> 
           let (mib,mip) = Global.lookup_inductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
-	      let nodep_constr = has_nodep_prod_after mip.mind_nparams in
+	      let nodep_constr = has_nodep_prod_after mib.mind_nparams in
 		if array_for_all nodep_constr mip.mind_nf_lc then
 		  let params=
 		    if mip.mind_nrealargs=0 then args else
-		      fst (list_chop mip.mind_nparams args) in
+		      fst (list_chop mib.mind_nparams args) in
 		    Some (hdapp,params,mip.mind_nrealargs)
 		else 
 		  None
@@ -233,7 +233,7 @@ let match_with_sigma_type t=
           if (Array.length (mib.mind_packets)=1) &&
 	    (mip.mind_nrealargs=0) &&
 	    (Array.length mip.mind_consnames=1) &&
-	    has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then
+	    has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
 	      (*allowing only 1 existential*) 
 	      Some (hdapp,args)
 	  else 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e30bb7e63..29fd46f3e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -288,7 +288,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
     | _ -> anomaly "compute_construtor_signatures"
   in 
   let (mib,mip) = Global.lookup_inductive ity in
-  let n = mip.mind_nparams in
+  let n = mib.mind_nparams in
   let lc =
     Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
   let lrecargs = dest_subterms mip.mind_recargs in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 42e18fadc..2da3e2cf5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -220,7 +220,7 @@ let declare_one_elimination ind =
   let env = Global.env () in
   let sigma = Evd.empty in
   let elim_scheme = Indrec.build_indrec env sigma ind in
-  let npars = mip.mind_nparams in
+  let npars = mib.mind_nparams_rec in
   let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in
   let kelim = mip.mind_kelim in
   (* in case the inductive has a type elimination, generates only one
@@ -373,15 +373,15 @@ let interp_mutual lparams lnamearconstrs finite =
 	 in
 
          (* Build the inductive entry *)
-	 { mind_entry_params = params';
-	   mind_entry_typename = name;
+	 { mind_entry_typename = name;
 	   mind_entry_arity = ar;
 	   mind_entry_consnames = constrnames;
 	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
   States.unfreeze fs;
-  notations, { mind_entry_record = false; 
+  notations, { mind_entry_params = params';
+	       mind_entry_record = false; 
 	       mind_entry_finite = finite; 
 	       mind_entry_inds = mispecvec }
   with e -> States.unfreeze fs; raise e
@@ -397,6 +397,7 @@ let declare_mutual_with_eliminations isrecord mie =
 (* Very syntactical equality *)
 let eq_la d1 d2 = match d1,d2 with
   | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') ->
+      (List.length nal = List.length nal') &&
       List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal'
       & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
   | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d6eb9cfc5..be815ffd6 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -84,3 +84,5 @@ val admit : unit -> unit
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+
+
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 8c71c0513..f10a461d6 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -35,48 +35,54 @@ let detype_param = function
      I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
 *)
 
-let abstract_inductive hyps inds =
+let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in 
   let nhyp = named_context_length hyps in
   let args = instance_from_named_context (List.rev hyps) in
   let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
   let inds' =
     List.map
-      (function (np,tname,arity,cnames,lc) -> 
+      (function (tname,arity,cnames,lc) -> 
 	let lc' = List.map (substl subs) lc in
 	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
 	let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
-        (np,tname,arity',cnames,lc''))
+        (tname,arity',cnames,lc''))
       	inds in
+  let nparams' = nparams + Array.length args in
+(* To be sure to be the same as before, should probably be moved to process_inductive *) 
+  let params' = let (_,arity,_,_) = List.hd inds' in 
+		let (params,_) = decompose_prod_n_assum nparams' arity in
+		  List.map detype_param params
+  in
+  let ind'' = 
   List.map 
-    (fun (nparams,a,arity,c,lc) ->
-      let nparams' = nparams + Array.length args in
-      let params, short_arity = decompose_prod_n_assum nparams' arity in
+    (fun (a,arity,c,lc) ->
+      let _, short_arity = decompose_prod_n_assum nparams' arity in
       let shortlc =
-	List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
-      let params' = List.map detype_param params in
-      { mind_entry_params = params';
-        mind_entry_typename = a;
+	List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+      { mind_entry_typename = a;
 	mind_entry_arity = short_arity;
 	mind_entry_consnames = c;
 	mind_entry_lc = shortlc })
     inds'
+  in (params',ind'')
+
 
 let process_inductive sechyps modlist mib =
+  let nparams = mib.mind_nparams in
   let inds = 
     array_map_to_list
       (fun mip ->
-	 let nparams = mip.mind_nparams in
 	 let arity = expmod_constr modlist mip.mind_user_arity in
 	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
-	 (nparams,
-	  mip.mind_typename,
+	 (mip.mind_typename,
 	  arity,
 	  Array.to_list mip.mind_consnames,
 	  Array.to_list lc))
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
-  let inds' = abstract_inductive sechyps' inds in
+  let (params',inds') = abstract_inductive sechyps' nparams inds in
   { mind_entry_record = mib.mind_record;
     mind_entry_finite = mib.mind_finite;
+    mind_entry_params = params';
     mind_entry_inds = inds' }
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ad41844ce..8b72d5b01 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -586,7 +586,7 @@ let error_bad_induction dep indid kind =
   str "is not allowed"
 
 let error_not_mutual_in_scheme () =
- str "Induction schemes is concerned only with mutually inductive types"
+ str "Induction schemes are concerned only with distinct mutually inductive types"
 
 let explain_inductive_error = function
   (* These are errors related to inductive constructions *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f6d8b6000..6b412ea68 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -146,7 +146,7 @@ let subst_projection fid l c =
 let declare_projections indsp coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let paramdecls = mip.mind_params_ctxt in
+  let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
@@ -223,13 +223,13 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let ind = applist (mkRel (1+List.length params+List.length fields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_typename = idstruc;
+    { mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let mie =
-    { mind_entry_record = true;
+    { mind_entry_params = List.map degenerate_decl params;
+      mind_entry_record = true;
       mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations true mie in