Effets de bords suite à la restructuration des inductives (cf Inductive)

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

6 files changed, 108 insertions, 143 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2fbfa70f7..36281359b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -3,6 +3,7 @@ open Util
 open Names
 open Generic
 open Term
+open Constant
 open Inductive
 open Environ
 open Sign
@@ -47,12 +48,11 @@ let rec_branch_scheme env isevars ((sp,j),_) typc recargs =
   in 
   crec (typc,recargs) 
     
-let branch_scheme env isevars isrec i (mind,args as appmind) = 
-  let typc = type_inst_construct env !isevars i appmind in 
+let branch_scheme env isevars isrec i (IndFamily (mis,params) as indf) = 
+  let typc = type_inst_construct i indf in 
   if isrec then
-    let mispec = lookup_mind_specif mind env in 
-    let recarg = (mis_recarg mispec).(i-1) in
-    rec_branch_scheme env isevars mind typc recarg
+    let recarg = (mis_recarg mis).(i-1) in
+    rec_branch_scheme env isevars (mis_inductive mis) typc recarg
   else 
     norec_branch_scheme env isevars typc
 
@@ -125,7 +125,7 @@ type matrix = equation list
 
 (* 1st argument of IsInd is the original ind before extracting the summary *)
 type tomatch_type =
-  | IsInd of constr * inductive_summary
+  | IsInd of constr * inductive_type
   | NotInd of constr
 
 type dependency_in_rhs = DepInRhs | NotDepInRhs
@@ -194,7 +194,7 @@ let to_mutind env sigma t =
   with Induc -> NotInd t
 
 let type_of_tomatch_type = function
-    IsInd (t,ind_data) -> t
+    IsInd (t,ind) -> t
   | NotInd t -> t
 
 let current_pattern eqn =
@@ -211,21 +211,8 @@ let remove_current_pattern eqn =
     | _::pats -> { eqn with patterns = pats }
     | [] -> anomaly "Empty list of patterns"
 
-let liftn_ind_data n depth md =
-  let mind' = 
-    let (ind_sp,ctxt) = md.mind in
-    (ind_sp, Array.map (liftn n depth) ctxt) in
-  { mind = mind';
-    nparams = md.nparams;
-    nrealargs = md.nrealargs;
-    nconstr = md.nconstr;
-    params = List.map (liftn n depth) md.params;
-    realargs = List.map (liftn n depth) md.realargs }
-
-let lift_ind_data n = liftn_ind_data n 1
-
 let liftn_tomatch_type n depth = function
-  | IsInd (t,ind) -> IsInd (liftn n depth t,liftn_ind_data n depth ind)
+  | IsInd (t,ind) -> IsInd (liftn n depth t,liftn_inductive_type n depth ind)
   | NotInd t -> NotInd (liftn n depth t)
 
 let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -233,20 +220,23 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
 let lift_tomatch n ((current,typ),info) =
   ((lift n current,lift_tomatch_type n typ),info)
 
-let substn_many_ind_data cv depth md =
-  let mind' = 
-    let (ind_sp,ctxt) = md.mind in
-    (ind_sp, Array.map (substn_many cv depth) ctxt) in
-  { mind = mind';
-    nparams = md.nparams;
-    nrealargs = md.nrealargs;
-    nconstr = md.nconstr;
-    params = List.map (substn_many cv depth) md.params;
-    realargs = List.map (substn_many cv depth) md.realargs }
+let substn_many_ind_instance cv depth mis = {
+  mis_sp = mis.mis_sp;
+  mis_mib = mis.mis_mib;
+  mis_tyi = mis.mis_tyi;
+  mis_args = Array.map (substn_many cv depth) mis.mis_args;
+  mis_mip = mis.mis_mip
+}
+
+let substn_many_ind_data cv depth (IndFamily (mis,params)) =
+  IndFamily (substn_many_ind_instance cv depth mis,
+	     List.map (substn_many cv depth) params)
 
 let substn_many_tomatch v depth = function
-  | IsInd (t,ind_data) ->
-      IsInd (substn_many v depth t,substn_many_ind_data v depth ind_data)
+  | IsInd (t,IndType (ind_data,realargs)) ->
+      IsInd (substn_many v depth t,
+	     IndType (substn_many_ind_data v depth ind_data,
+		      List.map (substn_many v depth) realargs))
   | NotInd t -> NotInd (substn_many v depth t)
 
 let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
@@ -489,15 +479,15 @@ let prepare_unif_pb typ cs =
   (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
   (Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
 
-let infer_predicate env isevars typs cstrs ind_data =
+let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
   (* Il faudra substituer les isevars a un certain moment *)
   let eqns = array_map2 prepare_unif_pb typs cstrs in
 
   (* First strategy: no dependencies at all *)
-  let (cclargs,_,typn) = eqns.(ind_data.nconstr -1) in
+  let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
   if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
   then
-    let (sign,_) = get_arity env !isevars ind_data in
+    let (sign,_) = get_arity env !isevars indf in
     let pred = lam_it (lift (List.length sign) typn) sign in
     (false,pred) (* true = dependent -- par défaut *)
   else
@@ -539,14 +529,14 @@ let rec weaken_predicate n pred =
   if n=0 then pred else match pred with
     | PrLetIn _ | PrCcl _ ->
 		    anomaly "weaken_predicate: only product can be weakened"
-    | PrProd ((dep,_,IsInd (_,ind_data)),pred) ->
+    | PrProd ((dep,_,IsInd (_,IndType(indf,realargs))),pred) ->
 	(* To make it more uniform, we apply realargs but they not occur! *)
-	let tm = (ind_data.realargs,if dep then Some (Rel n) else None) in
-	PrLetIn (tm, weaken_predicate (n-1)
-		   (lift_predicate ind_data.nrealargs pred))
+	let copt = if dep then Some (Rel n) else None in
+	PrLetIn ((realargs,copt), weaken_predicate (n-1)
+		   (lift_predicate (List.length realargs) pred))
     | PrProd ((dep,_,NotInd t),pred) ->
-	let tm = ([],if dep then Some (Rel n) else None) in
-	PrLetIn (tm, weaken_predicate (n-1) pred)
+	let copt = if dep then Some (Rel n) else None in
+	PrLetIn (([],copt), weaken_predicate (n-1) pred)
 
 let rec extract_predicate = function
   | PrProd ((_,na,t),pred) ->
@@ -555,16 +545,16 @@ let rec extract_predicate = function
   | PrLetIn ((args,None),pred) -> substl args (extract_predicate pred)
   | PrCcl ccl -> ccl
 
-let abstract_predicate env sigma ind_data = function
+let abstract_predicate env sigma indf = function
   | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
   | PrLetIn ((_,copt),pred) ->
-      let asign,_ = get_arity env sigma ind_data in
+      let asign,_ = get_arity env sigma indf in
       let sign =
 	List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
       let dep = copt<> None in
       let sign' =
 	if dep then
-	  let ind = build_dependent_inductive ind_data in
+	  let ind = build_dependent_inductive indf in
 	  let na = named_hd (Global.env()) ind Anonymous in
 	  (na,ind)::sign
 	else sign in
@@ -583,12 +573,12 @@ let specialize_predicate_match tomatchs cs = function
 	(* Ne perd-on pas des cas en ne posant pas true à la place de dep ? *)
 	(fun ((na,t),_) p -> PrProd ((dep,na,t),p)) tomatchs pred''
 
-let find_predicate env isevars p typs cstrs current ind_data =
+let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
   let (dep,pred) =
     match p with
-      | Some p -> abstract_predicate env !isevars ind_data p
-      | None -> infer_predicate env isevars typs cstrs ind_data in
-  let typ = applist (pred, ind_data.realargs) in
+      | Some p -> abstract_predicate env !isevars indf p
+      | None -> infer_predicate env isevars typs cstrs indf in
+  let typ = applist (pred, realargs) in
   if dep then (pred, applist (typ, [current]), dummy_sort)
   else (pred, typ, dummy_sort)
 
@@ -600,7 +590,7 @@ type inversion_problem =
   | Incompatible of int * (int * int)
   | Constraints of (int * constr) list
 
-let solve_constraints constr_info ind_data =
+let solve_constraints constr_info indt =
   (* TODO *)
   Constraints []
 
@@ -716,13 +706,14 @@ and match_current pb (n,tm) =
     | NotInd typ ->
 	check_all_variables typ pb.mat;
 	compile (shift_problem pb)
-    | IsInd (_,ind_data) ->
-	let cstrs = get_constructors pb.env !(pb.isevars) ind_data in
-	let eqns,defaults = group_equations ind_data.mind cstrs pb.mat in
+    | IsInd (_,(IndType(indf,realargs) as indt)) ->
+	let mis,_ = dest_ind_family indf in
+	let cstrs = get_constructors indf in
+	let eqns,defaults = group_equations (mis_inductive mis) cstrs pb.mat in
 	if array_for_all ((=) []) eqns
 	then compile (shift_problem pb)
 	else
-          let constraints = Array.map (solve_constraints ind_data) cstrs in
+          let constraints = Array.map (solve_constraints indt) cstrs in
 	  let pbs =
 	    array_map2 (build_branch pb defaults current) eqns cstrs in
 	  let tags = Array.map (pattern_status defaults) eqns in
@@ -731,9 +722,8 @@ and match_current pb (n,tm) =
 	  let brtyps = Array.map (fun j -> j.uj_type) brs in
 	  let (pred,typ,s) =
 	    find_predicate pb.env pb.isevars 
-	      pb.pred brtyps cstrs current ind_data in
-	  let ci = make_case_info
-		     (lookup_mind_specif ind_data.mind pb.env) None tags in
+	      pb.pred brtyps cstrs current indt in
+	  let ci = make_case_info mis None tags in
 	  { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
 	    uj_type = typ;
 	    uj_kind = s }
@@ -808,7 +798,7 @@ let rec find_row_ind = function
 exception NotCoercible
 
 let inh_coerce_to_ind isevars env ty tyi =
-  let (ntys,_) = splay_prod env !isevars (Instantiate.mis_arity (Global.lookup_mind_specif tyi)) in
+  let (ntys,_) = splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in
   let (_,evarl) =
     List.fold_right
       (fun (na,ty) (env,evl) ->
@@ -835,9 +825,9 @@ let coerce_row typing_fun isevars env row tomatch =
 	 with NotCoercible ->
 	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
 	   try
-	     let ind_data = find_inductive env !isevars j.uj_type in
+	     let mind,_ = find_minductype env !isevars j.uj_type in
 	     error_bad_constructor_loc cloc CCI
-	       (constructor_of_rawconstructor c) ind_data.mind
+	       (constructor_of_rawconstructor c) mind
 	   with Induc ->
 	     error_case_not_inductive_loc
 	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
@@ -857,9 +847,9 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
 
 let build_expected_arity env sigma isdep tomatchl sort =
   let cook n = function
-    | _,IsInd (_,ind_data) ->
-	let is = lift_ind_data n ind_data in
-	(build_dependent_inductive is, fst (get_arity env sigma is))
+    | _,IsInd (_,IndType(indf,_)) ->
+	let indf' = lift_inductive_family n indf in
+	(build_dependent_inductive indf', fst (get_arity env sigma indf'))
     | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
   in
   let rec buildrec n = function
@@ -876,13 +866,13 @@ let build_expected_arity env sigma isdep tomatchl sort =
 
 let build_initial_predicate isdep pred tomatchl =
   let cook n = function
-    | _,IsInd (_,ind_data) ->
-	let args = List.map (lift n) ind_data.realargs in
+    | _,IsInd (_,IndType(ind_data,realargs)) ->
+	let args = List.map (lift n) realargs in
 	if isdep then
 	  let ty = lift n (build_dependent_inductive ind_data) in
-	  (ind_data.nrealargs+1, (args,Some ty))
+	  (List.length realargs + 1, (args,Some ty))
 	else
-	  (ind_data.nrealargs, (args,None))
+	  (List.length realargs, (args,None))
     | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
   in
   let rec buildrec n pred = function
@@ -917,7 +907,7 @@ let rec eta_expand env sigma c t =
  *)
 let case_dependent env sigma loc predj tomatchs =
   let nb_dep_ity = function
-      (_,IsInd (_,ind_data)) -> ind_data.nrealargs
+      (_,IsInd (_,IndType(_,realargs))) -> List.length realargs
     | (c,NotInd t) ->
 	errorlabstrm "case_dependent" (error_case_not_inductive CCI env c t)
   in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3dbe65ff8..fbf77e402 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,6 +6,7 @@ open Names
 open Term
 open Evd
 open Environ
+open Inductive
 open Rawterm
 open Evarutil
 (*i*)
@@ -13,7 +14,7 @@ open Evarutil
 (* Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> 'a evar_defs -> bool -> int -> inductive * constr list -> constr
+  env -> 'a evar_defs -> bool -> int -> inductive_family -> constr
 
 (* Compilation of pattern-matching. *)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0f3a36153..091c14a2e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -102,24 +102,23 @@ let ids_of_env = Sign.ids_of_env
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive id =
-  let (refsp,tyi as indsp) =
+  let (indsp,_ as ind) =
     try 
-      let sp = Nametab.sp_of_id CCI id in
-      match global_operator sp id with
-	| MutInd ind_sp,_ -> ind_sp
+      match kind_of_term (global_reference CCI id) with
+	| IsMutInd (indsp,args) -> (indsp,args)
 	| _ -> errorlabstrm "indsp_of_id" 
 	    [< 'sTR ((string_of_id id)^" is not an inductive type") >]
     with Not_found -> 
       error ("Cannot find reference "^(string_of_id id))
   in
-  let mip = mind_nth_type_packet (Global.lookup_mind refsp) tyi in
-  let constr_lengths = Array.map List.length mip.mind_listrec in
+  let mis = Global.lookup_mind_specif ind in
+  let constr_lengths = Array.map List.length (mis_recarg mis) in
   (indsp,constr_lengths)
 
 let sp_of_spi (refsp,tyi) =
-  let mip = mind_nth_type_packet (Global.lookup_mind refsp) tyi in
+  let mip = Constant.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
   let (pa,_,k) = repr_path refsp in 
-  make_path pa mip.mind_typename k
+  make_path pa mip.Constant.mind_typename k
 
 (*
   let (_,mip) = mind_specif_of_mind_light spi in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 77c422b37..c4b757034 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -59,58 +59,40 @@ and whd_betaxtra x = applist(whrec x [])
 let lift_context n l = 
   let k = List.length l in 
   list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
-let prod_create env (a,b) = 
-  mkProd (named_hd env a Anonymous) a b
-let lambda_name env (n,a,b) = 
-  mkLambda (named_hd env a n) a b
-let lambda_create env (a,b) = 
-  mkLambda (named_hd env a Anonymous) a b
-let it_prod_name env = 
-  List.fold_left (fun c (n,t) -> prod_name env (n,t,c)) 
-let it_lambda_name env = 
-  List.fold_left (fun c (n,t) -> lambda_name env (n,t,c))
-
-let transform_rec loc env sigma cl (ct,pt) = 
-  let (mind,largs as appmind) = find_minductype env sigma ct in
-  let p = cl.(0)
-  and c = cl.(1)
-  and lf = Array.sub cl 2 ((Array.length cl) - 2) in
-  let mispec = lookup_mind_specif mind env in
-  let mI = mkMutInd mind in
+
+let transform_rec loc env sigma (p,c,lf) (indt,pt) = 
+  let (indf,realargs) = dest_ind_type indt in
+  let (mispec,params) = dest_ind_family indf in
+  let mI = mkMutInd (mis_inductive mispec) in
   let recargs = mis_recarg mispec in
-  let expn = Array.length recargs in
-  if Array.length lf <> expn then 
-    error_number_branches_loc loc CCI env c ct expn;
-  if is_recursive [mispec.mis_tyi] recargs then
-    let dep = find_case_dep_nparams env sigma (c,p) appmind pt in 
-    let ntypes = mis_ntypes mispec (* was mis_nconstr !?! *)
-    and tyi = mispec.mis_tyi 
-    and nparams = mis_nparams mispec in
-    let depFvec = Array.create ntypes (None : (bool * constr) option) in 
-    let _ = Array.set depFvec mispec.mis_tyi (Some(dep,Rel 1)) in 
-    let (pargs,realargs) = list_chop nparams largs in
-    let vargs = Array.of_list pargs in
-    let (_,typeconstrvec) = mis_type_mconstructs mispec in
+  let tyi = mis_index mispec in
+  if Array.length lf <> mis_nconstr mispec then 
+    error_number_branches_loc loc CCI env c
+      (mkAppliedInd indt) (mis_nconstr mispec);
+  if mis_is_recursive_subset [tyi] mispec then
+    let dep = find_case_dep_nparams env sigma (c,p) indf pt in 
+    let init_depFvec i = if i = tyi then Some(dep,Rel 1) else None in
+    let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
+    let constrs = get_constructors indf in
     (* build now the fixpoint *)
-    let realar =
-      hnf_prod_appvect env sigma "make_branch" (mis_arity mispec) vargs in
-    let lnames,_ = splay_prod env sigma realar in 
+    let lnames,_ = get_arity env sigma indf in
     let nar = List.length lnames in
+    let nparams = mis_nparams mispec in
     let ci = make_default_case_info mispec in
     let branches = 
       array_map3
 	(fun f t reca -> 
 	   whd_betaxtra
              (Indrec.make_rec_branch_arg env sigma
-                ((Array.map (lift (nar+2)) vargs),depFvec,nar+1)
+                (nparams,depFvec,nar+1)
                 f t reca))
-        (Array.map (lift (nar+2)) lf) typeconstrvec recargs 
+        (Array.map (lift (nar+2)) lf) constrs recargs 
     in 
     let deffix = 
       it_lambda_name env
 	(lambda_create env
-	   (appvect (mI,Array.append (Array.map (lift (nar+1)) vargs)
-                       (rel_vect 0 nar)),
+	   (applist (mI,List.append (List.map (lift (nar+1)) params)
+                       (rel_list 0 nar)),
             mkMutCaseA ci (lift (nar+2) p) (Rel 1) branches))
         (lift_context 1 lnames) 
     in
@@ -120,9 +102,9 @@ let transform_rec loc env sigma cl (ct,pt) =
       let typPfix = 
 	it_prod_name env
 	  (prod_create env
-	     (appvect (mI,(Array.append 
-			     (Array.map (lift nar) vargs)
-			     (rel_vect 0 nar))),
+	     (applist (mI,(List.append 
+			     (List.map (lift nar) params)
+			     (rel_list 0 nar))),
 	      (if dep then 
 		 applist (whd_beta_stack env sigma 
 			    (lift (nar+1) p) (rel_list 0 (nar+1)))
@@ -195,13 +177,10 @@ let wrong_number_of_cases_message loc env isevars (c,ct) expn =
   let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in
   error_number_branches_loc loc CCI env c ct expn
 
-let check_branches_message loc env isevars (c,ct) (explft,lft) = 
-  let n = Array.length explft and expn = Array.length lft in
-  if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn;
-  for i = 0 to n-1 do
+let check_branches_message loc env isevars c (explft,lft) = 
+  for i = 0 to Array.length explft - 1 do
     if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
       let c = nf_ise1 !isevars c
-      and ct = nf_ise1 !isevars ct 
       and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in
       error_ill_formed_branch_loc loc CCI env c i lfi 
 	(nf_betaiota env !isevars explft.(i))
@@ -397,7 +376,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
-  let {mind=mind;params=params;realargs=realargs} =
+  let (IndType (indf,realargs) as indt) = 
     try find_inductive env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
 	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
@@ -416,14 +395,13 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	    then error_cant_find_case_type_loc loc env cj.uj_val
 	    else
 	      try
-		let expti =
-		  Cases.branch_scheme env isevars isrec i (mind,params) in
+		let expti = Cases.branch_scheme env isevars isrec i indf in
 		let fj =
                   pretype (mk_tycon expti) env isevars lvar lmeta lf.(i-1) in
 		let efjt = nf_ise1 !isevars fj.uj_type in 
 		let pred = 
-		  Indrec.pred_case_ml_onebranch env !isevars isrec 
-		    (cj.uj_val,(mind,params,realargs)) (i,fj.uj_val,efjt) in
+		  Indrec.pred_case_ml_onebranch env !isevars isrec indt
+		    (i,fj.uj_val,efjt) in
 		if has_ise !isevars pred then findtype (i+1)
 		else 
 		  let pty = Retyping.get_type_of env !isevars pred in
@@ -432,13 +410,14 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	      with UserError _ -> findtype (i+1) in
 	    findtype 1 in
 
-  let evalct = nf_ise1 !isevars cj.uj_type
+  let evalct = find_inductive env !isevars cj.uj_type (*Pour normaliser evars*)
   and evalPt = nf_ise1 !isevars pj.uj_type in
 
   let (bty,rsty) =
     Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
   if Array.length bty <> Array.length lf then
-    wrong_number_of_cases_message loc env isevars (cj.uj_val,evalct)
+    wrong_number_of_cases_message loc env isevars 
+      (cj.uj_val,nf_ise1 !isevars cj.uj_type)
       (Array.length bty)
   else
     let lfj =
@@ -447,14 +426,14 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
           lf in
     let lfv = (Array.map (fun j -> j.uj_val) lfj) in
     let lft = (Array.map (fun j -> j.uj_type) lfj) in
-    check_branches_message loc env isevars (cj.uj_val,evalct) (bty,lft);
+    check_branches_message loc env isevars cj.uj_val (bty,lft);
     let v =
       if isrec
       then 
-	let rEC = Array.append [|pj.uj_val; cj.uj_val|] lfv in
-	transform_rec loc env !isevars rEC (evalct,evalPt)
+	transform_rec loc env !isevars(pj.uj_val,cj.uj_val,lfv) (evalct,evalPt)
       else
-	let ci = make_default_case_info (lookup_mind_specif mind env) in
+	let mis,_ = dest_ind_family indf in
+	let ci = make_default_case_info mis in
 	mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj) in
 
        {uj_val = v;
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 6eb095d53..96de2fc0a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -52,14 +52,14 @@ let rec type_of env cstr=
     | IsMutConstruct cstr -> 
         let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
     | IsMutCase (_,p,c,lf) ->
-        let ind_data =
+        let IndType (indf,realargs) =
           try find_inductive env sigma (type_of env c)
           with Induc -> anomaly "type_of: Bad inductive" in
-	let (aritysign,_) = get_arity env sigma ind_data in
+	let (aritysign,_) = get_arity env sigma indf in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
         let al =
 	  if List.length psign > List.length aritysign
-	  then ind_data.realargs@[c] else ind_data.realargs in
+	  then realargs@[c] else realargs in
         whd_betadeltaiota env sigma (applist (p,al))
     | IsLambda (name,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0240cdbc2..2f3b674f6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -94,15 +94,11 @@ let contract_cofix_use_function f cofix =
   	sAPPViList bodynum (array_last bodyvect) lbodies
     | _ -> assert false
 
-let mind_nparams env i =
-  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
-
 let reduce_mind_case_use_function env f mia =
   match mia.mconstr with 
     | DOPN(MutConstruct(ind_sp,i as cstr_sp),args) ->
-	let ind = inductive_of_constructor (cstr_sp,args) in
-	let nparams = mind_nparams env ind in
-	let real_cargs = snd(list_chop nparams mia.mcargs) in
+	let ncargs = (fst mia.mci).(i-1) in
+	let real_cargs = list_lastn ncargs mia.mcargs in
 	applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
 	let cofix_def = contract_cofix_use_function f cofix in