petit nettoyage de kernel/inductive

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

11 files changed, 165 insertions, 140 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4d8c03d3e..41d6941a9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -92,7 +92,8 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
   in 
   crec env (List.rev cstr.cs_args,recargs) 
     
-let branch_scheme env isevars isrec ((ind,params) as indf) =
+let branch_scheme env isevars isrec indf =
+  let (ind,params) = dest_ind_family indf in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let cstrs = get_constructors env indf in 
   if isrec then
@@ -139,7 +140,7 @@ exception NotInferable of ml_case_error
 
 let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
   let pred =
-    let (ind,params) = indf in
+    let (ind,params) = dest_ind_family indf in
     let (mib,mip) = Inductive.lookup_mind_specif env ind in
     let recargs = mip.mind_listrec in
     if Array.length recargs = 0 then raise (NotInferable MlCaseAbsurd);
@@ -449,12 +450,12 @@ let unify_tomatch_with_patterns isevars env typ = function
 	 try
 	   IsInd (typ,find_rectype env (evars_of isevars) typ)
              (* will try to coerce later in check_and_adjust_constructor.. *)
-	 with Induc ->
+	 with Not_found ->
 	   NotInd (None,typ))
 	     (* error will be detected in check_all_variables *)
   | None -> 
       try IsInd (typ,find_rectype env (evars_of isevars) typ)
-      with Induc -> NotInd (None,typ)
+      with Not_found -> NotInd (None,typ)
 
 let coerce_row typing_fun isevars env cstropt tomatch =
   let j = typing_fun empty_tycon env tomatch in
@@ -939,7 +940,8 @@ let abstract_conclusion typ cs =
   let (sign,p) = decompose_prod_n n typ in
   lam_it p sign
 
-let infer_predicate loc env isevars typs cstrs ((mis,_) as indf) =
+let infer_predicate loc env isevars typs cstrs indf =
+  let (mis,_) = dest_ind_family indf in
   (* Il faudra substituer les isevars a un certain moment *)
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 45694a01b..287e78f76 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -33,7 +33,7 @@ exception PatternMatchingError of env * pattern_matching_error
 (*s Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> evar_defs -> bool -> inductive * constr list -> constr array
+  env -> evar_defs -> bool -> inductive_family -> constr array
 
 type ml_case_error =
   | MlCaseAbsurd
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 111e5a514..5300f1f9b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -166,39 +166,39 @@ let computable p k =
 
 
 
-let lookup_name_as_renamed ctxt t s =
+let lookup_name_as_renamed env t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | Prod (name,_,c') ->
-	(match concrete_name avoid env_names name c' with
+	(match concrete_name env avoid env_names name c' with
            | (Some id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match concrete_name avoid env_names name c' with
+	(match concrete_name env avoid env_names name c' with
            | (Some id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | Cast (c,_) -> lookup avoid env_names n c
     | _ -> None
-  in lookup (ids_of_named_context ctxt) empty_names_context 1 t
+  in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
 
-let lookup_index_as_renamed t n =
+let lookup_index_as_renamed env t n =
   let rec lookup n d c = match kind_of_term c with
     | Prod (name,_,c') ->
-	  (match concrete_name [] empty_names_context name c' with
+	  (match concrete_name env [] empty_names_context name c' with
                (Some _,_) -> lookup n (d+1) c'
              | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match concrete_name [] empty_names_context name c' with
+	  (match concrete_name env [] empty_names_context name c' with
              | (Some _,_) -> lookup n (d+1) c'
              | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | Cast (c,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
 
-let rec detype avoid env t =
+let rec detype tenv avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
@@ -212,23 +212,26 @@ let rec detype avoid env t =
     | Sort (Prop c) -> RSort (dummy_loc,RProp c)
     | Sort (Type u) -> RSort (dummy_loc,RType (Some u))
     | Cast (c1,c2) ->
-	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
-    | Prod (na,ty,c) -> detype_binder BProd avoid env na ty c
-    | Lambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
-    | LetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
+	RCast(dummy_loc,detype tenv avoid env c1,
+              detype tenv avoid env c2)
+    | Prod (na,ty,c) -> detype_binder tenv BProd avoid env na ty c
+    | Lambda (na,ty,c) -> detype_binder tenv BLambda avoid env na ty c
+    | LetIn (na,b,_,c) -> detype_binder tenv BLetIn avoid env na b c
     | App (f,args) ->
-	RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args)
+	RApp (dummy_loc,detype tenv avoid env f,
+              array_map_to_list (detype tenv avoid env) args)
     | Const sp -> RRef (dummy_loc, ConstRef sp)
     | Evar (ev,cl) ->
 	let f = REvar (dummy_loc, ev) in
-	RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl))
+	RApp (dummy_loc, f,
+              List.map (detype tenv avoid env) (Array.to_list cl))
     | Ind ind_sp ->
 	RRef (dummy_loc, IndRef ind_sp)
     | Construct cstr_sp ->
 	RRef (dummy_loc, ConstructRef cstr_sp)
     | Case (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
-	let tomatch = detype avoid env c in
+	let tomatch = detype tenv avoid env c in
 	let indsp = annot.ci_ind in
         let considl = annot.ci_pp_info.cnames in
         let k = annot.ci_pp_info.ind_nargs in
@@ -237,11 +240,11 @@ let rec detype avoid env t =
 	  if synth_type & computable p k & considl <> [||] then
 	    None
 	  else 
-	    Some (detype avoid env p) in
+	    Some (detype tenv avoid env p) in
 	let constructs = 
 	  Array.init (Array.length considl) (fun i -> (indsp,i+1)) in
 	let eqnv =
-	  array_map3 (detype_eqn avoid env) constructs consnargsl bl in
+	  array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in
 	let eqnl = Array.to_list eqnv in
 	let tag =
 	  if PrintingLet.active (indsp,consnargsl) then 
@@ -253,10 +256,10 @@ let rec detype avoid env t =
 	in 
 	RCases (dummy_loc,tag,pred,[tomatch],eqnl)
 	
-    | Fix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef
-    | CoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
+    | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef
+    | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef
 
-and detype_fix avoid env fixkind (names,tys,bodies) =
+and detype_fix tenv avoid env fixkind (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left
       (fun (avoid, env, l) na ->
@@ -264,11 +267,11 @@ and detype_fix avoid env fixkind (names,tys,bodies) =
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
   RRec(dummy_loc,fixkind,Array.of_list (List.rev lfi),
-       Array.map (detype avoid env) tys,
-       Array.map (detype def_avoid def_env) bodies)
+       Array.map (detype tenv avoid env) tys,
+       Array.map (detype tenv def_avoid def_env) bodies)
 
 
-and detype_eqn avoid env constr construct_nargs branch =
+and detype_eqn tenv avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
     if not (force_wildcard ()) or (dependent (mkRel 1) b) then
       let id = next_name_away_with_default "x" x avoid in
@@ -280,7 +283,7 @@ and detype_eqn avoid env constr construct_nargs branch =
     if n=0 then
       (dummy_loc, ids, 
        [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-       detype avoid env b)
+       detype tenv avoid env b)
     else
       match kind_of_term b with
 	| Lambda (x,_,b) -> 
@@ -305,15 +308,15 @@ and detype_eqn avoid env constr construct_nargs branch =
   in 
   buildrec [] [] avoid env construct_nargs branch
 
-and detype_binder bk avoid env na ty c =
+and detype_binder tenv bk avoid env na ty c =
   let na',avoid' =
-    if bk = BLetIn then concrete_let_name avoid env na c
+    if bk = BLetIn then concrete_let_name tenv avoid env na c
     else
-      match concrete_name avoid env na c with
+      match concrete_name tenv avoid env na c with
 	| (Some id,l') -> (Name id), l'
 	| (None,l')    -> Anonymous, l' in
-  let r =  detype avoid' (add_name na' env) c in
+  let r =  detype tenv avoid' (add_name na' env) c in
   match bk with
-    | BProd -> RProd (dummy_loc, na',detype [] env ty, r)
-    | BLambda -> RLambda (dummy_loc, na',detype [] env ty, r)
-    | BLetIn -> RLetIn (dummy_loc, na',detype [] env ty, r)
+    | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r)
+    | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r)
+    | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index f787da2ba..44992725f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -17,15 +17,14 @@ open Rawterm
 open Termops
 (*i*)
 
-(* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *)
+(* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *)
 (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
 
-val detype : identifier list -> names_context -> constr -> rawconstr
+val detype : env -> identifier list -> names_context -> constr -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed :
-  named_context -> constr -> identifier -> int option
-val lookup_index_as_renamed : constr -> int -> int option
+val lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val lookup_index_as_renamed : env -> constr -> int -> int option
 
 
 val force_wildcard : unit -> bool
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d52c7f643..cb51cecaf 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -59,13 +59,13 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
-  let indf = (ind, extended_rel_list 0 lnamespar) in
+  let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
   let constrs = get_constructors env indf in
 
   let rec add_branch env k = 
     if k = Array.length mip.mind_consnames then
       let nbprod = k+1 in
-      let indf = (ind,extended_rel_list nbprod lnamespar) in
+      let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in
       let lnamesar,_ = get_arity env indf in
       let ci = make_default_case_info env ind in
       it_mkLambda_or_LetIn_name env'
@@ -103,7 +103,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
  * on it with which predicate and which recursive function. 
  *)
 
-let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
+let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
   let make_prod = make_prod_dep dep in
   let nparams = List.length vargs in
   let process_pos env depK pk =
@@ -120,7 +120,8 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let (_,realargs) = list_chop nparams largs in
 	    let base = applist (lift i pk,realargs) in
             if depK then 
-	      mkApp (base, [|applist (mkRel (i+1),extended_rel_list 0 sign)|])
+	      Reduction.beta_appvect
+                base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
             else 
 	      base
       	| _ -> assert false 
@@ -133,12 +134,11 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs =
           let (optionpos,rest) = 
 	    match recargs with 
 	      | [] -> None,[] 
-	      | Param _ :: rest -> (None,rest)
-	      | Norec :: rest   -> (None,rest)
+	      | Mrec j :: rest when is_rec -> (depPvect.(j),rest)
 	      | Imbr _ :: rest  -> 
 		  Options.if_verbose warning "Ignoring recursive call"; 
 		  (None,rest) 
-	      | Mrec j :: rest -> (depPvect.(j),rest)
+              | _ :: rest -> (None, rest)
 	  in 
           (match optionpos with 
 	     | None -> 
@@ -167,7 +167,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
         let params = List.map (lift i) vargs in
         let co = applist (mkConstruct cs.cs_cstr,params@realargs) in
-	mkApp (c, [|co|])
+	Reduction.beta_appvect c [|co|]
       else c
   in
   let nhyps = List.length cs.cs_args in
@@ -258,9 +258,10 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	    let nctyi =
               Array.length mipi.mind_consnames in (* nb constructeurs du type *) 
 
-            (* arity in the context P1..P_nrec f1..f_nbconstruct *)
+            (* 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 indf = (indi,args) in
+	    let indf = make_ind_family(indi,args) in
 	    let lnames,_ = get_arity env indf in
 
 	    let nar = mipi.mind_nrealargs in
@@ -268,8 +269,11 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	    let dect = nar+nrec+nbconstruct in
 	    let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
 
-	    let args = extended_rel_list (decf+1) lnamespar in
-	    let constrs = get_constructors env (indi,args) in
+            (* 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 (decf+1) lnamespar in
+            let indf' = make_ind_family(indi,args') in
+	    let constrs = get_constructors env indf' in
 	    let branches = 
 	      array_map3
 		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
@@ -277,8 +281,6 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	    let j = (match depPvec.(tyi) with 
 		       | Some (_,c) when isRel c -> destRel c 
 		       | _ -> assert false) in
-	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
-	    let indf = (indi,args) in
 	    let deftyi = 
 	      it_mkLambda_or_LetIn_name env
 		(lambda_create env
@@ -325,7 +327,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	      let indf = (indi, vargs) in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
 	      let p_0 =
-		type_rec_branch dep env sigma (vargs,depPvec,i+j) tyi cs recarg
+		type_rec_branch
+                  true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
 	      in 
 	      mkLambda_string "f" p_0
 		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
@@ -398,8 +401,9 @@ let instanciate_type_indrec_scheme sort npars term =
     match kind_of_term elim with
       | Prod (n,t,c) -> 
 	  if np = 0 then 
-            let t' = change_sort_arity sort t
-	    in mkProd (n, t', c), mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
+            let t' = change_sort_arity sort t in
+            mkProd (n, t', c),
+            mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
 	  else 
             let c',term' = drec (np-1) c in
 	    mkProd (n, t, c'), mkLambda (n, t, term')
@@ -451,38 +455,32 @@ let build_indrec env sigma ind =
 (* To handle old Case/Match syntax in Pretyping                       *)
 
 (***********************************)
-(* To interpret the Match operator *)
+(* To interpret Case and Match operators *)
 
-(* TODO: check that we can drop universe constraints ? *)
-let type_mutind_rec env sigma (IndType (indf,realargs) as indt) pj c = 
+let type_rec_branches recursive env sigma indt pj c = 
+  let IndType (indf,realargs) = indt in
   let p = pj.uj_val in
   let (ind,params) = dest_ind_family indf in
   let tyi = snd ind in
   let (mib,mip) = lookup_mind_specif env ind in
-  if mis_is_recursive_subset [tyi] mip then
-    let (dep,_) = find_case_dep_nparams env (c,pj) indf in 
-    let init_depPvec i = if i = tyi then Some(dep,p) else None in
-    let depPvec = Array.init mib.mind_ntypes init_depPvec in
-    let vargs = Array.of_list params in
-    let constructors = get_constructors env indf in
-    let recargs = mip.mind_listrec in
-    let lft = array_map2 (type_rec_branch dep env sigma (params,depPvec,0) tyi)
-                constructors recargs in
-    (lft,
-     if dep then applist(p,realargs@[c]) 
-     else applist(p,realargs) )
-  else 
+  let is_rec = recursive && mis_is_recursive_subset [tyi] mip in
+  let dep = is_dependent_elimination env pj.uj_type indf in 
+  let init_depPvec i = if i = tyi then Some(dep,p) else None in
+  let depPvec = Array.init mib.mind_ntypes init_depPvec in
+  let vargs = Array.of_list params in
+  let constructors = get_constructors env indf in
+  let recargs = mip.mind_listrec in
+  let lft =
+    array_map2
+      (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi)
+      constructors recargs in
+  (lft,
+   if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) 
+   else Reduction.beta_appvect p (Array.of_list realargs))
+(* Non recursive case. Pb: does not deal with unification
     let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
     (p,ra)
-
-let type_rec_branches recursive env sigma indt pj c =
-  if recursive then 
-    type_mutind_rec env sigma indt pj c
-  else 
-    let IndType((ind,params),rargs) = indt in
-    let (p,ra,_) = type_case_branches env (ind,params@rargs) pj c in
-    (p,ra)
-
+*)
 
 (*s Eliminations. *)
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6bf4813c2..cb1e7d3ee 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -190,19 +190,17 @@ let build_branch_type env dep p cs =
 
 (**************************************************)
 
-exception Induc
-
 let extract_mrectype t =
   let (t, l) = decompose_app t in
   match kind_of_term t with
     | Ind ind -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_mrectype env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
   match kind_of_term t with
     | Ind ind -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_rectype env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
@@ -211,7 +209,7 @@ let find_rectype env sigma c =
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
         let (par,rargs) = list_chop mip.mind_nparams l in
         IndType((ind, par),rargs)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_inductive env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
@@ -219,7 +217,7 @@ let find_inductive env sigma c =
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
         (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_coinductive env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
@@ -227,28 +225,27 @@ let find_coinductive env sigma c =
     | Ind ind
         when not (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
         (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 
 (***********************************************)
 (* find appropriate names for pattern variables. Useful in the
    Case tactic. *)
 
-let is_dep_arity env kelim predty t = 
-  let rec srec (pt,t) =
+let is_dep_arity env kelim predty nodep_ar = 
+  let rec srec pt nodep_ar =
     let pt' = whd_betadeltaiota env Evd.empty pt in
-    let t' = whd_betadeltaiota env Evd.empty t in
-    match kind_of_term pt', kind_of_term t' with
-      | Prod (_,a1,a2), Prod (_,a1',a2') -> srec (a2,a2')
+    match kind_of_term pt', kind_of_term nodep_ar with
+      | Prod (_,a1,a2), Prod (_,a1',a2') -> srec a2 a2'
       | Prod (_,a1,a2), _ -> true
       | _ -> false in 
-  srec (predty,t)
+  srec predty nodep_ar
 
-let is_dep env predty (ind,args) =
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let params = fst (list_chop mip.mind_nparams args) in
+let is_dependent_elimination env predty indf =
+  let (ind,params) = indf in
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
   let kelim = mip.mind_kelim in
-  let arsign,s = get_arity env (ind,params) in
+  let arsign,s = get_arity env indf in
   let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
   is_dep_arity env kelim predty glob_t
 
@@ -261,17 +258,29 @@ let set_pattern_names env ind brv =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
-      (fun c -> List.length (fst (decompose_prod c)) - mip.mind_nparams)
+      (fun c ->
+        rel_context_length (fst (decompose_prod_assum c)) -
+        mip.mind_nparams)
       mip.mind_nf_lc in
   array_map2 (set_names env) arities brv
 
 
 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
-  if is_dep env pj.uj_type indspec then
-    (set_pattern_names env (fst indspec) lbrty, conclty)
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let params = fst (list_chop mip.mind_nparams args) in
+  if is_dependent_elimination env pj.uj_type (ind,params) then
+    (set_pattern_names env ind lbrty, conclty)
   else (lbrty, conclty)
 
+(* Type of Case predicates *)
+let arity_of_case_predicate env (ind,params) dep k =
+  let arsign,_ = get_arity env (ind,params) in
+  let mind = build_dependent_inductive env (ind,params) in
+  let concl = if dep then mkArrow mind (mkSort k) else mkSort k in
+  it_mkProd_or_LetIn concl arsign
+
 (***********************************************)
 (* Guard condition *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 09c81c7d7..b807c2d7f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -15,9 +15,9 @@ open Environ
 open Evd
 
 (* An inductive type with its parameters *)
-type inductive_family = inductive * constr list
-val make_ind_family : 'a * 'b -> 'a * 'b
-val dest_ind_family : 'a * 'b -> 'a * 'b
+type inductive_family
+val make_ind_family : inductive * constr list -> inductive_family
+val dest_ind_family : inductive_family -> inductive * constr list
 val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
 val lift_inductive_family  : int -> inductive_family -> inductive_family
 val substnl_ind_family :
@@ -49,23 +49,31 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :
   inductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
-val get_constructors :
-  env -> inductive * constr list -> constructor_summary array
-val get_arity : env -> inductive * constr list -> Sign.arity
+val get_arity        : env -> inductive_family -> Sign.arity
+val get_constructors : env -> inductive_family -> constructor_summary array
 val build_dependent_constructor : constructor_summary -> constr
-val build_dependent_inductive   : env -> inductive * constr list -> constr
+val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature :
-  env -> bool -> inductive * constr list -> Sign.rel_context
-val make_arity : env -> bool -> inductive * constr list -> sorts -> types
+  env -> bool -> inductive_family -> Sign.rel_context
+val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
-exception Induc
+(* Raise Not_found if not given an valid inductive type *)
 val extract_mrectype : constr -> inductive * constr list
 val find_mrectype    : env -> evar_map -> constr -> inductive * constr list
 val find_rectype     : env -> evar_map -> constr -> inductive_type
 val find_inductive   : env -> evar_map -> constr -> inductive * constr list
 val find_coinductive : env -> evar_map -> constr -> inductive * constr list
 
+(********************)
+(* Determines if a case predicate type corresponds to dependent elimination *)
+val is_dependent_elimination :
+  env -> types -> inductive_family -> bool
+
+(* Builds the case predicate arity (dependent or not) *)
+val arity_of_case_predicate :
+  env -> inductive_family -> bool -> sorts -> types
+
 val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
@@ -73,4 +81,5 @@ val make_case_info :
   env -> inductive -> case_style option -> pattern_source array -> case_info
 val make_default_case_info : env -> inductive -> case_info
 
+(********************)
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d28db7510..11ddc43cd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,7 +43,8 @@ let lift_context n l =
 
 let transform_rec loc env sigma (pj,c,lf) indt = 
   let p = pj.uj_val in
-  let ((ind,params) as indf,realargs) = dest_ind_type indt in
+  let (indf,realargs) = dest_ind_type indt in
+  let (ind,params) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let mI = mkInd ind in
   let recargs = mip.mind_listrec in
@@ -54,9 +55,8 @@ let transform_rec loc env sigma (pj,c,lf) indt =
     (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
      error_number_branches_loc loc env sigma cj nconstr);
   if mis_is_recursive_subset [tyi] mip then
-    let (dep,_) =
-      find_case_dep_nparams env
-        (nf_evar sigma c, j_nf_evar sigma pj) indf in 
+    let dep =
+      is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in 
     let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
     let depFvec = Array.init mib.mind_ntypes init_depFvec in
     (* build now the fixpoint *)
@@ -322,10 +322,16 @@ let rec pretype tycon env isevars lvar lmeta = function
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
-	with Induc ->
+	with Not_found ->
           error_case_not_inductive_loc loc env (evars_of isevars) cj in
-      let pj = match po with
-	| Some p -> pretype empty_tycon env isevars lvar lmeta p
+      let (dep,pj) = match po with
+	| Some p ->
+            let pj = pretype empty_tycon env isevars lvar lmeta p in
+            let dep = is_dependent_elimination env pj.uj_type indf in
+            let ar =
+              arity_of_case_predicate env indf dep (Type (new_univ())) in
+            let _ = the_conv_x_leq env isevars pj.uj_type ar in
+            (dep, pj)
 	| None -> 
             (* get type information from type of branches *)
 	    let expbr = Cases.branch_scheme env isevars isrec indf in
@@ -337,7 +343,8 @@ let rec pretype tycon env isevars lvar lmeta = function
                 (* may be Type while Prop or Set would be expected *)
 	        match tycon with
 		  | Some pred ->
-                      Retyping.get_judgment_of env (evars_of isevars) pred
+                      (false,
+                       Retyping.get_judgment_of env (evars_of isevars) pred)
 	          | None ->
                       let sigma = evars_of isevars in
                       error_cant_find_case_type_loc loc env sigma cj.uj_val
@@ -355,13 +362,11 @@ let rec pretype tycon env isevars lvar lmeta = function
                       Retyping.get_type_of env (evars_of isevars) pred in
 		    let pj = { uj_val = pred; uj_type = pty } in
                     let _ = option_app (the_conv_x_leq env isevars pred) tycon
-                    in pj
+                    in (false,pj)
 		with Cases.NotInferable _ -> findtype (i+1) in
 	    findtype 0 in
       let pj = j_nf_evar (evars_of isevars) pj in
 
-      let (dep,_) = find_case_dep_nparams env (cj.uj_val,pj) indf in
-
       let pj =
 	if dep then pj else
 	  let n = List.length realargs in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a87354d65..2380b94c8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -70,7 +70,7 @@ let typeur sigma metamap =
         (* TODO: could avoid computing the type of branches *)
         let i =
           try find_rectype env (type_of env c)
-          with Induc -> anomaly "type_of: Bad recursive type" in
+          with Not_found -> anomaly "type_of: Bad recursive type" in
         let pj = { uj_val = p; uj_type = type_of env p } in
         let (_,ty,_) = type_case_branches env i pj c in
         ty
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index e861ebbe4..790abaa43 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -638,25 +638,25 @@ let occur_rel p env id =
   try lookup_name_of_rel p env = Name id
   with Not_found -> false (* Unbound indice : may happen in debug *)
 
-let occur_id env id0 c =
+let occur_id env nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
     | Const sp when basename sp = id0 -> raise Occur
     | Ind ind_sp
-	when basename (path_of_inductive (Global.env()) ind_sp) = id0 ->
+	when basename (path_of_inductive env ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when basename (path_of_constructor (Global.env()) cstr_sp) = id0 ->
+	when basename (path_of_constructor env cstr_sp) = id0 ->
         raise Occur
-    | Rel p when p>n & occur_rel (p-n) env id0 -> raise Occur
+    | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c
   in 
   try occur 1 c; false
   with Occur -> true
 
-let next_name_not_occuring name l env_names t =
+let next_name_not_occuring env name l env_names t =
   let rec next id =
-    if List.mem id l or occur_id env_names id t then next (lift_ident id)
+    if List.mem id l or occur_id env env_names id t then next (lift_ident id)
     else id
   in 
   match name with
@@ -664,16 +664,16 @@ let next_name_not_occuring name l env_names t =
     | Anonymous -> id_of_string "_"
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name l env_names n c =
+let concrete_name env l env_names n c =
   if n = Anonymous & not (dependent (mkRel 1) c) then
     (None,l)
   else
-    let fresh_id = next_name_not_occuring n l env_names c in
+    let fresh_id = next_name_not_occuring env n l env_names c in
     let idopt = if dependent (mkRel 1) c then (Some fresh_id) else None in
     (idopt, fresh_id::l)
 
-let concrete_let_name l env_names n c =
-  let fresh_id = next_name_not_occuring n l env_names c in
+let concrete_let_name env l env_names n c =
+  let fresh_id = next_name_not_occuring env n l env_names c in
   (Name fresh_id, fresh_id::l)
 
 let global_vars env ids = Idset.elements (global_vars_set env ids)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2a3e8b29c..e47570f47 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -126,15 +126,15 @@ val names_of_rel_context : env -> names_context
 (* sets of free identifiers *)
 type used_idents = identifier list
 val occur_rel : int -> name list -> identifier -> bool
-val occur_id : name list -> identifier -> constr -> bool
+val occur_id : env -> name list -> identifier -> constr -> bool
 
 val next_name_not_occuring :
-  name -> identifier list -> name list -> constr -> identifier
+  env -> name -> identifier list -> name list -> constr -> identifier
 val concrete_name :
-  identifier list -> name list -> name ->
+  env -> identifier list -> name list -> name ->
   constr -> identifier option * identifier list
 val concrete_let_name :
-  identifier list -> name list ->
+  env -> identifier list -> name list ->
   name -> constr -> name * identifier list
 val global_vars : env -> constr -> identifier list
 val rename_bound_var : env -> identifier list -> types -> types