Nouveaux types 'constructor' et 'inductive' dans Term;

les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.


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

11 files changed, 84 insertions, 147 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 30c88a227..0d48e9872 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -83,13 +83,14 @@ let prod_name env (n,a,b) =
 let ctxt_of_ids ids =
   Array.of_list (List.map (function id -> VAR id) ids)
 
-let mutconstruct_of_constructor (((sp,i),j),args) = 
-  mkMutConstruct sp i j (ctxt_of_ids args)
-let mutind_of_constructor (((sp,i),_),args) = mkMutInd sp i (ctxt_of_ids args)
-let mutind_of_ind ((sp,i),args) = mkMutInd sp i args
-
-let ith_constructor i {mind=((sp, tyi), cl)} = mkMutConstruct sp tyi i cl
+let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids)
 
+let mutconstruct_of_rawconstructor c = 
+  mkMutConstruct (constructor_of_rawconstructor c)
+let inductive_of_rawconstructor c =
+  inductive_of_constructor (constructor_of_rawconstructor c)
+let ith_constructor i mind =
+  mkMutConstruct (ith_constructor_of_inductive mind i)
 
 (* determines whether is a predicate or not *)
 let is_predicate ind_data = (ind_data.nrealargs > 0)
@@ -110,7 +111,7 @@ let lift_lfconstr n (s,c) = (s+n,c)
 (* Partial check on patterns *)
 let check_pat_arity env = function
   | PatCstr (loc, (cstr_sp,ids as c), args, name) ->
-      let ity = mutind_of_constructor c in
+      let ity = inductive_of_rawconstructor c in
       let nparams = mis_nparams (lookup_mind_specif ity env) in
       let tyconstr =
 	type_of_constructor env Evd.empty (cstr_sp,ctxt_of_ids ids) in
@@ -127,10 +128,10 @@ let rec constr_of_pat isevars env = function
   | PatVar (_,Anonymous) -> VAR (id_of_string "_")
   (* invalid_arg "constr_of_pat"*)
   | PatCstr(_,c,args,name) ->
-      let ity = mutind_of_constructor c in
+      let ity = inductive_of_rawconstructor c in
       let mispec = Global.lookup_mind_specif ity in 
       let nparams = mis_nparams mispec in
-      let c = mutconstruct_of_constructor c in
+      let c = mutconstruct_of_rawconstructor c in
       let exl =
 	list_tabulate
 	  (fun _ ->
@@ -284,7 +285,9 @@ type info_flow = INH | SYNT | INH_FIRST
    the non-dependent case is applied to an object of dependent type.
 *)
 
-type tomatch = IsInd of constr * mutind | MayBeNotInd of constr * constr
+type tomatch =
+  | IsInd of constr * inductive_summary
+  | MayBeNotInd of constr * constr
 
 let to_mutind env sigma c t =
   try IsInd (c,try_mutind_of env sigma t)
@@ -475,17 +478,17 @@ let patt_are_var =
     (fun r -> match row_current r with PatVar _ -> true |_ -> false)
 
 
-let check_pattern (ind_sp,_) row =
+let check_pattern (ind_sp,_ as ind) row =
   match row_current row with
       PatVar (_,id) -> ()
-    | PatCstr (loc,(cstr_sp,_),args,name) ->
-        if inductive_of_constructor cstr_sp <> ind_sp then
-	  error_bad_constructor_loc loc CCI cstr_sp ind_sp
+    | PatCstr (loc,(cstr_sp,ids),args,name) ->
+        if inductive_path_of_constructor_path cstr_sp <> ind_sp then
+	  error_bad_constructor_loc loc CCI (cstr_sp,ctxt_of_ids ids) ind
 
 let check_patt_are_correct ity mat = List.iter (check_pattern ity) mat 
 
 (*The only variables that patterns can share with the environment are 
-  parameters of inducive definitions!. Thus patterns should also be 
+  parameters of inductive definitions!. Thus patterns should also be 
   lifted when pushing inthe context. *)
 
 
@@ -641,7 +644,7 @@ let submat depcase isevars env i ind_data params current mat =
   let constraints = matching concl_realargs ind_data.realargs in
 *)
   let nbargs_iconstr = constructor_numargs ind_data i in
-  let ci = ith_constructor i ind_data in
+  let ci = ith_constructor i ind_data.mind in
 
   let expand_row r =
     let build_new_row subpatts name =
@@ -670,7 +673,7 @@ let submat depcase isevars env i ind_data params current mat =
 	    | Anonymous -> None
 	    | Name id -> Some (mychange_name_rel env current id) in
 	  (envopt, [build_new_row None name])
-      | PatCstr(_,c,largs,alias) when mutconstruct_of_constructor c = ci ->
+      | PatCstr(_,c,largs,alias) when mutconstruct_of_rawconstructor c = ci ->
 	(* Avant: il y aurait eu un problème si un des largs contenait
    	   un "_". Un problème aussi pour inférer les params des
    	   constructeurs sous-jacents, car on n'avait pas accès ici
@@ -696,7 +699,7 @@ let submat depcase isevars env i ind_data params current mat =
 
 
 type status =
-  | Match_Current of (constr * mutind * info_flow) (* "(", ")" needed... *)
+  | Match_Current of (constr * inductive_summary * info_flow) (* "(", ")" needed... *)
   | Any_Tomatch | All_Variables
   | Any_Tomatch_Dep | All_Variables_Dep | Solve_Constraint 
 
@@ -958,7 +961,7 @@ let abstracted_inductive sigma env ind_data =
 
   let params0 = List.map (lift m) params in
   let args0 = rel_list 0 m in
-  let t = applist (mutind_of_ind ity, params0@args0) in
+  let t = applist (mkMutInd ity, params0@args0) in
   let na = named_hd (Global.env()) t Anonymous in
   (na,t)::sign, {ind_data with params=params0;realargs=args0}
 
@@ -1016,19 +1019,19 @@ let apply_to_dep env sigma pred = function
 
 (* analogue strategy as Christine's MLCASE *)
 let find_implicit_pred sigma ith_branch_builder env (current,ind_data,_) =
-  let {fullmind=ct;nconstr=nconstr} = ind_data in
+  let {nconstr=nconstr;mind=mind;params=params;realargs=realargs} = ind_data in
   let isrec = false in 
   let rec findtype i = 
     if i > nconstr then raise (CasesError (env, CantFindCaseType current))
     else 
       try
- 	(let expti = Indrec.branch_scheme env sigma isrec i ct in
+ 	(let expti = Indrec.branch_scheme env sigma isrec i (mind,params) in
        	let _,bri= ith_branch_builder i  in
        	let fi = bri.uj_type in 
        	let efit = nf_ise1 sigma fi in 
        	let pred =
           Indrec.pred_case_ml_onebranch env sigma isrec 
-            (current,ct) (i,bri.uj_val,efit) in
+            (current,(mind,params,realargs)) (i,bri.uj_val,efit) in
  	if has_ise sigma pred then error"isevar" else pred)
       with UserError _ -> findtype (i+1)
   in findtype 1  
@@ -1109,7 +1112,7 @@ let type_one_branch dep env sigma ind_data p im =
              let (_,vargs) = array_chop (nparams+1) lAV in
 	     let c1 = appvect (lift n p,vargs) in
 	     if dep then 
-	       let co = ith_constructor i ind_data in
+	       let co = ith_constructor i ind_data.mind in
 	       applist
 		 (c1,[applist(co,((List.map (lift n) params)@(rel_list 0 n)))])
 	     else c1
@@ -1244,7 +1247,7 @@ and build_dep_branch trad env gd bty (current,ind_data,info) i =
  let l,_ = splay_prod env sigma ty in
  let lpatt = List.map (fun (na,ty) -> (to_mutind env sigma xtra_tm ty,SYNT)) l in
  let ngd =  pop_and_prepend_tomatch lpatt gd in
- let ci_param = applist (ith_constructor i ind_data, params) in
+ let ci_param = applist (ith_constructor i ind_data.mind, params) in
 
  let rnnext_env0,next_mat = submat ngd.case_dep trad.isevars env i 
                                     ind_data params current ngd.mat in
@@ -1322,7 +1325,7 @@ and build_nondep_branch trad env gd next_pred bty
                   mat = ncurgd.mat}) in
  let nncur = lift k ncur in
  let lp = List.map (lift k) params in
- let ci = applist (ith_constructor i ind_data, lp@(rel_list 0 k)) in 
+ let ci = applist (ith_constructor i ind_data.mind, lp@(rel_list 0 k)) in 
 
  let rnnext_env0,next_mat=submat ngd.case_dep trad.isevars next_env i 
                                  ind_data lp nncur ngd.mat in
@@ -1411,7 +1414,7 @@ and match_current trad env (current,ind_data,info as cji) gd =
       match List.map (build_ith_branch gd) (interval 1 nconstr) with
 	  [] -> (*  nconstr=0 *)
 	   (context env),
-	  mkMutCaseA (ci_of_mind (mutind_of_ind ity)) 
+	  mkMutCaseA (ci_of_mind (mkMutInd ity)) 
 		    (eta_reduce_if_rel p) current [||]
 
       | (bre1,f)::lenv_f as brl ->
@@ -1429,7 +1432,7 @@ and match_current trad env (current,ind_data,info as cji) gd =
 	in
 	check_conv 0;
         (common_prefix_ctxt (context env) bre1,
-         mkMutCaseA (ci_of_mind (mutind_of_ind ity))
+         mkMutCaseA (ci_of_mind (mkMutInd ity))
 	   (eta_reduce_if_rel (nf_ise1 !(trad.isevars) p))
 	   current lf) in
     newenv,
@@ -1512,7 +1515,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd =
 		    (snd (build_ith_branch nenv ngd1 i)).uj_val)
                  (interval 1 nconstr) in
       let case_exp =
- 	mkMutCaseA (ci_of_mind (mutind_of_ind ity)) (eta_reduce_if_rel np)
+ 	mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel np)
 	  current (Array.of_list lf) in
       let (na,ty),_ = uncons_rel_env (context nenv) in
       let rescase = lambda_name env (na,body_of_type ty,case_exp) in
@@ -1524,7 +1527,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd =
        let lf = List.map (fun i -> 
 			      (snd (build_ith_branch nenv ngd1 i)).uj_val)
                   (interval 1 nconstr) in
-       let rescase = mkMutCaseA (ci_of_mind (mutind_of_ind ity)) 
+       let rescase = mkMutCaseA (ci_of_mind (mkMutInd ity)) 
 		 (eta_reduce_if_rel np) current (Array.of_list lf) in
        let casetyp = whd_beta nenv !(trad.isevars) (applist (np,args)) in
        (context nenv),rescase,casetyp
@@ -1544,7 +1547,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd =
          * this (Rel 1) by initial value will be done by the application 
          *)
         let case_exp =
-           mkMutCaseA (ci_of_mind (mutind_of_ind ity)) np1 (Rel 1) (Array.of_list lf) in
+           mkMutCaseA (ci_of_mind (mkMutInd ity)) np1 (Rel 1) (Array.of_list lf) in
         let nenv2,rescase = elam_and_popl_named n (context nenv1) case_exp in
 	let casetyp = whd_beta nenv1 !(trad.isevars) (applist (np,args@[(Rel 1)])) in
         nenv2,rescase,casetyp
@@ -1678,7 +1681,7 @@ let check_coercibility isevars env ty indty =
 let check_pred_correctness isevars env tomatchl pred =
   let cook n = function
     | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data))
-      -> (applist (mutind_of_ind ity,(List.map (lift n) params)
+      -> (applist (mkMutInd ity,(List.map (lift n) params)
 		   @(rel_list 0 ind_data.nrealargs)),
 	  lift n (whd_beta env !isevars (applist (arity,params))))
     | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent"
@@ -1703,7 +1706,7 @@ let check_pred_correctness isevars env tomatchl pred =
 let build_expected_arity isdep env sigma tomatchl sort =
   let cook n = function
     | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data))
-      -> (applist (mutind_of_ind ity,(List.map (lift n) params)
+      -> (applist (mkMutInd ity,(List.map (lift n) params)
 		   @(rel_list 0 ind_data.nrealargs)),
 	  lift n (whd_beta env sigma (applist (arity,params))))
     | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent"
@@ -1795,15 +1798,6 @@ let rec find_row_ind = function
   | PatVar _ :: l -> find_row_ind l
   | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
 
-
-let find_pretype mat =
-  let lpatt = List.map (fun r -> List.hd r.patterns) mat in
-  match find_row_ind lpatt with
-    Some (_,c) -> mutind_of_constructor c
-  | None -> anomalylabstrm "find_pretype" 
-       	[<'sTR "Expecting a patt. in constructor form and found empty list">]
-
-
 (* We do the unification for all the rows that contain
  * constructor patterns. This is what we do at the higher level of patterns.
  * For nested patterns, we do this unif when we ``expand'' the matrix, and we
@@ -1825,7 +1819,7 @@ let inh_coerce_to_ind isevars env ty tyi =
 	   (push_rel (na,(make_typed ty s)) env,
 	    fst (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl))
       ntys (env,[]) in
-  let expected_typ = applist (tyi,evarl) in
+  let expected_typ = applist (mkMutInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
   if Evarconv.the_conv_x_leq env isevars expected_typ ty then ty
@@ -1836,7 +1830,7 @@ let coerce_row trad env row tomatch =
   let j = trad.pretype mt_tycon env tomatch in
   match find_row_ind row with
       Some (cloc,(cstr,_ as c)) ->
-	(let tyi = mutind_of_constructor c in
+	(let tyi = inductive_of_rawconstructor c in
 	 try 
 	   let indtyp = inh_coerce_to_ind trad.isevars env j.uj_type tyi in
 	   IsInd (j.uj_val,try_mutind_of env !(trad.isevars) j.uj_type)
@@ -1844,7 +1838,8 @@ let coerce_row trad env row tomatch =
 	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
 	   try
 	     let ind_data = try_mutind_of env !(trad.isevars) j.uj_type in
-	     error_bad_constructor_loc cloc CCI cstr (fst ind_data.mind)
+	     error_bad_constructor_loc cloc CCI
+	       (constructor_of_rawconstructor c) ind_data.mind
 	   with Induc ->
 	     error_case_not_inductive_loc
 	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 80fa10520..792a66fe9 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -14,8 +14,8 @@ open Generic
 (* usage qque peu general: utilise aussi dans record *)
 
 type cte_typ = 
-  | NAM_Var of identifier 
-  | NAM_SP of section_path 
+  | NAM_Var of identifier
+  | NAM_SP of section_path
   | NAM_Construct of constructor_path
 
 let cte_of_constr = function  
@@ -30,7 +30,7 @@ type cl_typ =
   | CL_FUN
   | CL_Var of identifier
   | CL_SP of section_path 
-  | CL_IND of section_path * int
+  | CL_IND of inductive_path
 
 type cl_info_typ = {
   cL_STR : string;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index a4bf0ee8f..fe7fb437d 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -16,7 +16,7 @@ type cl_typ =
   | CL_FUN 
   | CL_Var of identifier 
   | CL_SP of section_path
-  | CL_IND of section_path * int
+  | CL_IND of inductive_path
 
 type cl_info_typ = {
   cL_STR : string;
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f55aaf69a..af42d3cd4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -80,8 +80,8 @@ let split_evar_to_arrow sigma c =
   let dsp = path_of_const (body_of_type dom) in
   let rsp = path_of_const (body_of_type rng) in
   (sigma3,
-   mkCast (mkConst dsp args) dummy_sort,
-   mkCast (mkConst rsp (array_cons (mkRel 1) args)) dummy_sort)
+   mkCast (mkConst (dsp,args)) dummy_sort,
+   mkCast (mkConst (rsp,array_cons (mkRel 1) args)) dummy_sort)
 
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 1292ad75c..9944f55a8 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -31,7 +31,7 @@ val error_case_not_inductive_loc :
 (* Pattern-matching errors *)
 
 val error_bad_constructor_loc : 
-  loc -> path_kind -> constructor_path -> inductive_path -> 'b
+  loc -> path_kind -> constructor -> inductive -> 'b
 
 val error_wrong_numarg_constructor_loc : 
   loc -> path_kind -> constructor_path -> int -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4391a7fe6..59716c5d6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -71,17 +71,18 @@ 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 (mI,largs as mind) = find_minductype env sigma ct in
+  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 mI env in 
+  let mispec = lookup_mind_specif mind env in
+  let mI = mkMutInd mind 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) mind pt in 
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) appmind pt in 
     let ntypes = mis_nconstr mispec 
     and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
@@ -241,8 +242,8 @@ let pretype_ref loc isevars env = function
 | RVar id -> pretype_var loc env id
 
 | RConst (sp,ids) ->
-    let cstr = mkConst sp (ctxt_of_ids ids) in
-    make_judge cstr (type_of_constant env !isevars cstr)
+    let cst = (sp,ctxt_of_ids ids) in
+    make_judge (mkConst cst) (type_of_constant env !isevars cst)
 
 | RAbst sp -> failwith "Pretype: abst doit disparaître"
 (*
@@ -267,18 +268,17 @@ let pretype_ref loc isevars env = function
 *)
 | REVar (sp,ids) -> error " Not able to type terms with dependent subgoals"
 (* Not able to type goal existential yet
-    let cstr = mkConst sp (ctxt_of_ids ids) in
+    let cstr = mkConst (sp,ctxt_of_ids ids) in
     make_judge cstr (type_of_existential env !isevars cstr)
 *)
-| RInd ((sp,i),ids) ->
-    let cstr = mkMutInd sp i (ctxt_of_ids ids) in
-    make_judge cstr (type_of_inductive env !isevars cstr)
+| RInd (ind_sp,ids) ->
+    let ind = (ind_sp,ctxt_of_ids ids) in
+    make_judge (mkMutInd ind) (type_of_inductive env !isevars ind)
  
-| RConstruct (((sp,i),j) as cstr_sp,ids) ->
-    let ctxt = ctxt_of_ids ids in
-    let (typ,kind) =
-      destCast (type_of_constructor env !isevars (cstr_sp,ctxt)) in
-    {uj_val=mkMutConstruct sp i j ctxt; uj_type=typ; uj_kind=kind}
+| RConstruct (cstr_sp,ids) ->
+    let cstr = (cstr_sp,ctxt_of_ids ids) in
+    let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
+    {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind}
 
 (* pretype vtcon isevars env constr tries to solve the *)
 (* existential variables in constr in environment env with the *)
@@ -373,8 +373,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype mt_tycon env isevars c in
-  let (mind,_) =
-    try find_mrectype env !isevars cj.uj_type
+  let {mind=mind;params=params;realargs=realargs} =
+    try try_mutind_of 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
   let pj = match po with
@@ -392,12 +392,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 = Indrec.branch_scheme env !isevars isrec i cj.uj_type in
+		let expti =
+		  Indrec.branch_scheme env !isevars isrec i (mind,params) in
 		let fj = pretype (mk_tycon expti) env isevars 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,cj.uj_type) (i,fj.uj_val,efjt) in
+		    (cj.uj_val,(mind,params,realargs)) (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
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e51919f2f..7d5417829 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -10,37 +10,6 @@ open Reduction
 open Environ
 open Typeops
 
-(* A light version of mind_specif_of_mind *)
-
-type mutind_id = inductive_path * constr array
-
-type mutind =
-    {fullmind : constr;
-     mind : mutind_id;
-     nparams : int;
-     nrealargs : int;
-     nconstr : int;
-     params : constr list;
-     realargs : constr list;
-     arity : constr}
-
-(* raise Induc if not an inductive type *)
-let try_mutind_of env sigma ty =
-  let (mind,largs) = find_mrectype env sigma ty in
-  let mispec = lookup_mind_specif mind env in 
-  let nparams = mis_nparams mispec in
-  let (params,realargs) = list_chop nparams largs in 
-  {fullmind = ty;
-   mind     = (let (sp,i,cv) = destMutInd mind in (sp,i),cv);
-   nparams  = nparams;
-   nrealargs = List.length realargs;
-   nconstr  = mis_nconstr mispec;
-   params   = params;
-   realargs = realargs;
-   arity    = Instantiate.mis_arity mispec}
-
-
-(********  A light version of type_of *********)
 type metamap = (int * constr) list
 
 let rec is_dep_case env sigma (pt,ar) =
@@ -85,13 +54,11 @@ let rec type_of env cstr=
     | IsVar id -> body_of_type (snd (lookup_var id env))
 
     | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
-    | IsConst _ -> (body_of_type (type_of_constant env sigma cstr))
+    | IsConst c -> (body_of_type (type_of_constant env sigma c))
     | IsEvar _ -> type_of_existential env sigma cstr
-    | IsMutInd _ -> (body_of_type (type_of_inductive env sigma cstr))
-    | IsMutConstruct (sp,i,j,args) -> 
-        let (typ,kind) =
-	  destCast (type_of_constructor env sigma (((sp,i),j),args))
-        in typ
+    | IsMutInd ind -> (body_of_type (type_of_inductive env sigma ind))
+    | IsMutConstruct cstr -> 
+        let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
     | IsMutCase (_,p,c,lf) ->
         let {realargs=args;arity=arity;nparams=n} =
           try try_mutind_of env sigma (type_of env c)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 354771e6e..036cd53f0 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -17,27 +17,3 @@ type metamap = (int * constr) list
 val get_type_of : env -> 'a evar_map -> constr -> constr
 val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
 val get_sort_of : env -> 'a evar_map -> constr -> sorts
-
-(*i The following should be merged with mind_specif and put elsewhere 
-    Note : it needs Reduction i*)
-
-(* A light version of [mind_specif] *)
-
-(* Invariant: We have\\
-   -- Hnf (fullmind) = DOPN(AppL,[|coremind;..params..;..realargs..|])\\
-   -- with mind  = MutInd ((sp,i),localvars) for some sp, i, localvars
- *)
-type mutind_id = inductive_path * constr array
-
-type mutind = {
-  fullmind : constr;
-  mind : mutind_id;
-  nparams : int;
-  nrealargs : int;
-  nconstr : int;
-  params : constr list;
-  realargs : constr list;
-  arity : constr }
-
-(* [try_mutind_of sigma t] raise Induc if [t] is not an inductive type *)
-val try_mutind_of : env -> 'a Evd.evar_map -> constr -> mutind
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ad33549ca..92fb27a23 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -55,9 +55,6 @@ let make_elim_fun f largs =
   with Elimconst | Failure _ -> 
     raise Redelimination
 
-let mind_nparams env i =
-  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
-
 (* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
    the reduction using this extra information *)
 
@@ -93,10 +90,13 @@ 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((indsp,tyindx),i),_) ->
-	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+    | 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
 	applist (mia.mlf.(i-1),real_cargs)
@@ -325,7 +325,7 @@ let one_step_reduce env sigma =
 let reduce_to_mind env sigma t = 
   let rec elimrec t l = 
     match whd_castapp_stack t [] with
-      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
+      | (DOPN(MutInd mind,args),_) -> ((mind,args),t,prod_it t l)
       | (DOPN(Const _,_),_) -> 
           (try 
 	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
@@ -346,6 +346,5 @@ let reduce_to_mind env sigma t =
  elimrec t []
 
 let reduce_to_ind env sigma t =
-  let (mind,redt,c) = reduce_to_mind env sigma t in 
-  (Declare.mind_path mind, redt, c)
-
+  let ((ind_sp,_),redt,c) = reduce_to_mind env sigma t in 
+  (Declare.path_of_inductive_path ind_sp, redt, c)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index a555667e6..bd20e8b7b 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -18,7 +18,7 @@ val nf : 'a reduction_function
 val one_step_reduce : 'a reduction_function
 
 val reduce_to_mind : 
-  env -> 'a evar_map -> constr -> constr * constr * constr
+  env -> 'a evar_map -> constr -> inductive * constr * constr
 
 val reduce_to_ind : 
   env -> 'a evar_map -> constr -> section_path * constr * constr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7c32a124c..afc11aaf8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -42,15 +42,14 @@ let rec execute mf env sigma cstr =
         else 
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
-    | IsConst _ ->
-        make_judge cstr (type_of_constant env sigma cstr)
+    | IsConst c ->
+        make_judge cstr (type_of_constant env sigma c)
 	  
-    | IsMutInd _ ->
-	make_judge cstr (type_of_inductive env sigma cstr)
+    | IsMutInd ind ->
+	make_judge cstr (type_of_inductive env sigma ind)
 	  
-    | IsMutConstruct (sp,i,j,args) -> 
-	let (typ,kind) =
-	  destCast (type_of_constructor env sigma (((sp,i),j),args)) in
+    | IsMutConstruct cstruct -> 
+	let (typ,kind) = destCast (type_of_constructor env sigma cstruct) in
         { uj_val = cstr; uj_type = typ; uj_kind = kind }
 	  
     | IsMutCase (_,p,c,lf) ->