petit nettoyage de kernel/inductive

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

28 files changed, 337 insertions, 364 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index be8f14203..a6db1a5ab 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -137,7 +137,7 @@ let tuple_ref dep n =
 
 let trad_binder avoid nenv = function
   | CC_untyped_binder -> RHole None
-  | CC_typed_binder ty -> Detyping.detype avoid nenv ty
+  | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
   | [] -> ([],avoid,nenv)
@@ -207,21 +207,22 @@ let rawconstr_of_prog p =
       	let n = List.length l in
       	let cl = List.map (trad avoid nenv) l in
       	let tuple = tuple_ref dep n in
-	let tyl = List.map (Detyping.detype avoid nenv) tyl in
+	let tyl = List.map (Detyping.detype (Global.env()) avoid nenv) tyl in
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
     | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	let ty = Detyping.detype avoid nenv ty in
+	let ty = Detyping.detype (Global.env()) avoid nenv ty in
 	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
-	Detyping.detype avoid nenv c
+	Detyping.detype (Global.env()) avoid nenv c
 
     | CC_hole c -> 
-	RCast (dummy_loc, RHole None, Detyping.detype avoid nenv c)
+	RCast (dummy_loc, RHole None,
+               Detyping.detype (Global.env()) avoid nenv c)
 
   in
   trad [] empty_names_context p
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index c23394e8c..b369bbf31 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1421,7 +1421,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1 (* List.nth targ (mis_index dmi)*)  in
@@ -1503,13 +1503,13 @@ and  hd_is_mind t ti =
     try (let env = Global.env() in
          let IndType (indf,targ) = find_rectype env Evd.empty t in
 	 let ncti= Array.length(get_constructors env indf) in
-	 let (ind,_) = indf in
+	 let (ind,_) = dest_ind_family indf in
          let (mib,mip) = lookup_mind_specif env ind in
 	 (string_of_id mip.mind_typename) = ti)
     with _ -> false
 and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
-  let (ind,_) = indf in
+  let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let p = mip.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
@@ -1539,7 +1539,7 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
@@ -1589,7 +1589,7 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b4a74061f..b45e501eb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,69 +18,45 @@ open Environ
 open Reduction
 open Type_errors
 
-exception Induc
-
-(* raise Induc if not an inductive type *)
+(* raise Not_found if not an inductive type *)
 let lookup_mind_specif env (sp,tyi) =
-  let mib =
-    try Environ.lookup_mind sp env
-    with Not_found -> raise Induc in
+  let mib = Environ.lookup_mind sp env in
   if tyi >= Array.length mib.mind_packets then
     error "Inductive.lookup_mind_specif: invalid inductive index";
   (mib, mib.mind_packets.(tyi))
 
-let lookup_recargs env ind =
-  let (mib,mip) = lookup_mind_specif env ind in
-  Array.map (fun mip -> mip.mind_listrec) mib.mind_packets
-
-let lookup_subterms env (_,i as ind) =
-  (lookup_recargs env ind).(i)
-
 let find_rectype env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
         when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 (***********************************************************************)
 
-type inductive_instance = {
-  mis_sp : section_path;
-  mis_mib : mutual_inductive_body;
-  mis_tyi : int;
-  mis_mip : one_inductive_body }
-
-let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
-
-let lookup_mind_instance (sp,tyi) env =
-  let (mib,mip) = lookup_mind_specif env (sp,tyi) in
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_mip = mip }
-
 (* Build the substitution that replaces Rels by the appropriate *)
 (* inductives *)
-let ind_subst mispec =
-  let ntypes = mispec.mis_mib.mind_ntypes in
-  let make_Ik k = mkInd (mispec.mis_sp,ntypes-k-1) in 
+let ind_subst mind mib =
+  let ntypes = mib.mind_ntypes in
+  let make_Ik k = mkInd (mind,ntypes-k-1) in 
   list_tabulate make_Ik ntypes
 
-(* Instantiate both section variables and inductives *)
-let constructor_instantiate mispec c =
-  let s = ind_subst mispec in
+(* Instantiate inductives in constructor type *)
+let constructor_instantiate mind mib c =
+  let s = ind_subst mind mib in
   type_app (substl s) c
 
 (* Instantiate the parameters of the inductive type *)
@@ -102,13 +78,13 @@ let instantiate_params t args sign =
   if rem_args <> [] then fail();
   type_app (substl subs) ty
 
-let full_inductive_instantiate (mispec,params) t =
-  instantiate_params t params mispec.mis_mip.mind_params_ctxt
+let full_inductive_instantiate mip params t =
+  instantiate_params t params mip.mind_params_ctxt
 
-let full_constructor_instantiate (mispec,params) =
-  let inst_ind = constructor_instantiate mispec in
+let full_constructor_instantiate (((mind,_),mib,mip),params) =
+  let inst_ind = constructor_instantiate mind mib in
   (fun t ->
-    instantiate_params (inst_ind t) params mispec.mis_mip.mind_params_ctxt)
+    instantiate_params (inst_ind t) params mip.mind_params_ctxt)
 
 (***********************************************************************)
 (***********************************************************************)
@@ -118,71 +94,47 @@ let full_constructor_instantiate (mispec,params) =
 (* Type of an inductive type *)
 
 let type_of_inductive env i =
-  let mis = lookup_mind_instance i env in
-  let hyps = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_user_arity
-
-(* The same, with parameters instantiated *)
-let get_arity (mispec,params as indf) =
-  let arity = mispec.mis_mip.mind_nf_arity in
-  destArity (full_inductive_instantiate indf arity)
+  let (_,mip) = lookup_mind_specif env i in
+  mip.mind_user_arity
 
 (***********************************************************************)
 (* Type of a constructor *)
 
 let type_of_constructor env cstr =
   let ind = inductive_of_constructor cstr in
-  let mispec = lookup_mind_instance ind env in
-  let specif = mispec.mis_mip.mind_user_lc in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
-  let nconstr = mis_nconstr mispec in
+  let nconstr = Array.length mip.mind_consnames in
   if i > nconstr then error "Not enough constructors in the type";
-  constructor_instantiate mispec specif.(i-1)
+  constructor_instantiate (fst ind) mib specif.(i-1)
 
 let arities_of_constructors env ind = 
-  let mispec = lookup_mind_instance ind env in
-  let specif = mispec.mis_mip.mind_user_lc in
-  Array.map (constructor_instantiate mispec) specif
+  let (mib,mip) = lookup_mind_specif env ind in
+  let specif = mip.mind_nf_lc in
+  Array.map (constructor_instantiate (fst ind) mib) specif
 
 
 
-(* gives the vector of constructors and of 
-   types of constructors of an inductive definition 
-   correctly instanciated *)
+(***********************************************************************)
 
-let mis_nf_constructor_type i mispec =
-  let nconstr = mis_nconstr mispec in
-  if i > nconstr then error "Not enough constructors in the type";
-  constructor_instantiate mispec mispec.mis_mip.mind_nf_lc.(i-1)
-   
-(*s Useful functions *)
-
-type constructor_summary = {
-  cs_cstr : constructor;
-  cs_params : constr list;
-  cs_nargs : int;
-  cs_args : rel_context;
-  cs_concl_realargs : constr array
-}
-
-let process_constructor ((mispec,params) as indf) j typi =
-  let typi = full_constructor_instantiate indf typi in
-  let (args,ccl) = decompose_prod_assum typi in
-  let (_,allargs) = decompose_app ccl in
-  let (_,vargs) = list_chop mispec.mis_mip.mind_nparams allargs in
-  { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) (j+1);
-    cs_params = params;
-    cs_nargs = rel_context_length args;
-    cs_args = args;
-    cs_concl_realargs = Array.of_list vargs }
-
-let get_constructors ((mispec,params) as indf) =
-  let constr_tys = mispec.mis_mip.mind_nf_lc in
-  Array.mapi (process_constructor indf) constr_tys
+let is_info_arity env c =
+  match dest_arity env c with
+    | (_,Prop Null) -> false 
+    | (_,Prop Pos)  -> true 
+    | (_,Type _)    -> true
 
-(***********************************************************************)
+let error_elim_expln env kp ki =
+  if is_info_arity env kp && not (is_info_arity env ki) then
+    NonInformativeToInformative
+  else 
+    match (kind_of_term kp,kind_of_term ki) with 
+      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
+      | _ -> WrongArity
 
-(* Type of case branches *)
+exception Arity of (constr * constr * arity_error) option
+
+(* Type of case predicates *)
 
 let local_rels ctxt =
   let (rels,_) =
@@ -196,48 +148,23 @@ let local_rels ctxt =
   in
   rels
 
-let build_dependent_constructor cs =
-  applist
-    (mkConstruct cs.cs_cstr,
-     (List.map (lift cs.cs_nargs) cs.cs_params)@(local_rels cs.cs_args))
+(* Get type of inductive, with parameters instantiated *)
+let get_arity mip params =
+  let arity = mip.mind_nf_arity in
+  destArity (full_inductive_instantiate mip params arity)
 
-let build_dependent_inductive ((mis, params) as indf) =
-  let arsign,_ = get_arity indf in
-  let nrealargs = mis.mis_mip.mind_nrealargs in
+let build_dependent_inductive ind mip params =
+  let arsign,_ = get_arity mip params in
+  let nrealargs = mip.mind_nrealargs in
   applist 
-    (mkInd (mis_inductive mis),
-     (List.map (lift nrealargs) params)@(local_rels arsign))
-
-(* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type dep p cs =
-  let args =
-    if dep then
-      Array.append cs.cs_concl_realargs [|build_dependent_constructor cs|]
-    else
-      cs.cs_concl_realargs in
-  let base = beta_appvect (lift cs.cs_nargs p) args in
-  it_mkProd_or_LetIn base cs.cs_args
-
-
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
+    (mkInd ind, (List.map (lift nrealargs) params)@(local_rels arsign))
 
-let error_elim_expln env kp ki =
-  if is_info_arity env kp && not (is_info_arity env ki) then
-    NonInformativeToInformative
-  else 
-    match (kind_of_term kp,kind_of_term ki) with 
-      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
-      | _ -> WrongArity
 
-exception Arity of (constr * constr * arity_error) option
-
-
-let is_correct_arity env kelim (c,pj) indf t = 
-  let rec srec (pt,t) u =
+let is_correct_arity env c pj ind mip params = 
+  let kelim = mip.mind_kelim in
+  let arsign,s = get_arity mip params in
+  let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
+  let rec srec pt t u =
     let pt' = whd_betadeltaiota env pt in
     let t' = whd_betadeltaiota env t in
     match kind_of_term pt', kind_of_term t' with
@@ -245,18 +172,18 @@ let is_correct_arity env kelim (c,pj) indf t =
           let univ =
             try conv env a1 a1'
             with NotConvertible -> raise (Arity None) in
-          srec (a2,a2') (Constraint.union u univ)
+          srec a2 a2' (Constraint.union u univ)
       | Prod (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env a2 in 
           let ksort = match kind_of_term k with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (Arity None) in
-	  let ind = build_dependent_inductive indf in
+	  let dep_ind = build_dependent_inductive ind mip params in
           let univ =
-            try conv env a1 ind
+            try conv env a1 dep_ind
             with NotConvertible -> raise (Arity None) in
           if List.exists ((=) ksort) kelim then
-	    ((true,k), Constraint.union u univ)
+	    (true, Constraint.union u univ)
           else 
 	    raise (Arity (Some(k,t',error_elim_expln env k t')))
       | k, Prod (_,_,_) ->
@@ -266,11 +193,11 @@ let is_correct_arity env kelim (c,pj) indf t =
             | Sort s -> family_of_sort s 
             | _ ->  raise (Arity None) in
           if List.exists ((=) ksort) kelim then 
-	    (false, pt'), u
+	    (false, u)
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env pt' t')))
   in 
-  try srec (pj.uj_type,t) Constraint.empty
+  try srec pj.uj_type nodep_ar Constraint.empty
   with Arity kinds ->
     let create_sort = function 
       | InProp -> mkProp
@@ -281,33 +208,52 @@ let is_correct_arity env kelim (c,pj) indf t =
       (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
       @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*)
     in 
-    let ind = mis_inductive (fst indf) in
     error_elim_arity env ind listarity c pj kinds
 
 
-let find_case_dep_nparams env (c,pj) (ind,params) =
-  let indf = lookup_mind_instance ind env in
-  let kelim = indf.mis_mip.mind_kelim in
-  let arsign,s = get_arity (indf,params) in
-  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
-  let ((dep,_),univ) =
-    is_correct_arity env kelim (c,pj) (indf,params) glob_t in
-  (dep,univ)
+(***********************************************************************)
+(* Type of case branches *)
 
+(* [p] is the predicate, [i] is the constructor number (starting from 0),
+   and [cty] is the type of the constructor (params not instantiated) *)
+let build_branches_type ind mib mip params dep p =
+  let build_one_branch i cty =
+    let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in
+    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 cargs =
+      if dep then
+        let cstr = ith_constructor_of_inductive ind (i+1) in
+        let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
+        vargs @ [dep_cstr]
+      else
+        vargs in
+    let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+    it_mkProd_or_LetIn base args in
+  Array.mapi build_one_branch mip.mind_nf_lc
+
+(* [p] is the predicate, [c] is the match object, [realargs] is the
+   list of real args of the inductive type *)
+let build_case_type dep p c realargs =
+  let args = if dep then realargs@[c] else realargs in
+  beta_appvect p (Array.of_list args)
 
-let type_case_branches env (mind,largs) pj c =
-  let mispec = lookup_mind_instance mind env in 
-  let nparams = mispec.mis_mip.mind_nparams in
+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 (params,realargs) = list_chop nparams largs in
-  let indf = (mispec,params) in
   let p = pj.uj_val in
-  let (dep,univ) = find_case_dep_nparams env (c,pj) (mind,params) in
-  let constructs = get_constructors indf in
-  let lc = Array.map (build_branch_type dep p) constructs in
-  let args = if dep then realargs@[c] else realargs in
-  (lc, beta_appvect p (Array.of_list args), univ)
+  let (dep,univ) = is_correct_arity env c pj ind 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)
 
 
+(***********************************************************************)
+(* Checking the case annotation is relevent *)
+
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
@@ -363,6 +309,10 @@ type guard_env =
     lst     : (int * (size * recarg list array)) list;
   }
 
+let lookup_recargs env ind =
+  let (mib,mip) = lookup_mind_specif env ind in
+  Array.map (fun mip -> mip.mind_listrec) mib.mind_packets
+
 let make_renv env minds recarg (_,tyi as ind) =
   let mind_recvec = lookup_recargs env ind in 
   let lcx = mind_recvec.(tyi)  in
@@ -423,6 +373,8 @@ let subterm_var p renv =
    correct envs and decreasing args.
 *)
 
+let lookup_subterms env (_,i as ind) =
+  (lookup_recargs env ind).(i)
 
 let imbr_recarg_expand env (sp,i as ind_sp) lrc =
   let recargs = lookup_subterms env ind_sp in
@@ -719,7 +671,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) = 
                   try find_inductive env a 
-                  with Induc -> raise_err i RecursionNotOnInductiveType in
+                  with Not_found -> raise_err i RecursionNotOnInductiveType in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
             else anomaly "check_one_fix: Bad occurrence of recursive call"
@@ -763,10 +715,9 @@ let check_one_cofix env nbfix def deftype =
       | Prod (x,a,b) ->
 	  codomain_is_coind (push_rel (x, None, a) env) b 
       | _ -> 
-	  try
-	    find_coinductive env b
-          with Induc ->
-	    raise (CoFixGuardError (CodomainNotInductiveType b))
+	  (try find_coinductive env b
+           with Not_found ->
+	     raise (CoFixGuardError (CodomainNotInductiveType b)))
   in
   let (mind, _) = codomain_is_coind env deftype in
   let (sp,tyi) = mind in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 720ae3e4a..719205331 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -16,22 +16,20 @@ open Declarations
 open Environ
 (*i*)
 
-exception Induc
-
 (*s Extracting an inductive type from a construction *)
 
 (* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_rectype], [find_inductive] and [find_coinductive]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
-   They raise [Induc] if not convertible to a recursive type. *)
+   They raise [Not_found] if not convertible to a recursive type. *)
 
 val find_rectype     : env -> types -> inductive * constr list
 val find_inductive   : env -> types -> inductive * constr list
 val find_coinductive : env -> types -> inductive * constr list
 
 (*s Fetching information in the environment about an inductive type.
-    Raises Induc if the inductive type is not found. *)
+    Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif :
   env -> inductive -> mutual_inductive_body * one_inductive_body
 
@@ -66,9 +64,3 @@ val check_case_info : env -> inductive -> case_info -> unit
 (*s Guard conditions for fix and cofix-points. *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
-
-(********************)
-(* TODO: remove (used in pretyping only...) *)
-val find_case_dep_nparams :
-  env -> constr * unsafe_judgment -> inductive * constr list ->
-    bool * constraints
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index ce62acdf8..9d63dc7dd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -282,7 +282,7 @@ let check_branch_types env cj (lft,explft) =
 let judge_of_case env ci pj cj lfj =
   let indspec =
     try find_rectype env cj.uj_type
-    with Induc -> error_case_not_inductive env cj in
+    with Not_found -> error_case_not_inductive env cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3076213e5..dcabd954c 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -128,8 +128,9 @@ let pr_ref_label = function (* On triche sur le contexte *)
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
-let pr_pattern_env env t = gentermpr (Termast.ast_of_pattern env t)
-let pr_pattern t = pr_pattern_env empty_names_context t
+let pr_pattern_env tenv env t =
+  gentermpr (Termast.ast_of_pattern tenv env t)
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
 
 let rec gentacpr gt =
   Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 967fa5306..ff5929279 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -42,7 +42,7 @@ val pr_inductive    : env -> inductive -> std_ppcmds
 val pr_global       : global_reference -> std_ppcmds
 val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
-val pr_pattern_env  : names_context -> constr_pattern -> std_ppcmds
+val pr_pattern_env  : env -> names_context -> constr_pattern -> std_ppcmds
 
 val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index a22f20ae7..547dcd759 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -303,7 +303,7 @@ let ast_of_constr at_top env t =
     else Reductionops.local_strong strip_outer_cast t in
   let avoid = if at_top then ids_of_context env else [] in
   ast_of_raw 
-    (Detyping.detype avoid (names_of_rel_context env) t')
+    (Detyping.detype env avoid (names_of_rel_context env) t')
 
 let ast_of_constant env sp =
   let a = ast_of_constant_ref sp in
@@ -329,7 +329,7 @@ let decompose_binder_pattern = function
   | PLetIn(na,b,c) -> Some (BLetIn,na,b,c)
   | _ -> None
 
-let rec ast_of_pattern env = function
+let rec ast_of_pattern tenv env = function
   | PRef ref -> ast_of_ref ref
 
   | PVar id -> ast_of_ident id
@@ -348,44 +348,47 @@ let rec ast_of_pattern env = function
       let (f,args) = 
 	skip_coercion (function PRef r -> Some r | _ -> None)
 	  (f,Array.to_list args) in
-      let astf = ast_of_pattern env f in
-      let astargs = List.map (ast_of_pattern env) args in
+      let astf = ast_of_pattern tenv env f in
+      let astargs = List.map (ast_of_pattern tenv env) args in
       (match f with 
 	 | PRef ref -> ast_of_app (implicits_of_global ref) astf astargs
 	 | _        -> ast_of_app [] astf astargs)
 
   | PSoApp (n,args) ->
       ope("SOAPP",(ope ("META",[num n])):: 
-		  (List.map (ast_of_pattern env) args))
+		  (List.map (ast_of_pattern tenv env) args))
 
   | PLetIn (na,b,c) ->
-      let c' = ast_of_pattern (add_name na env) c in
-      ope("LETIN",[ast_of_pattern env b;slam(idopt_of_name na,c')])
+      let c' = ast_of_pattern tenv (add_name na env) c in
+      ope("LETIN",[ast_of_pattern tenv env b;slam(idopt_of_name na,c')])
 		
   | PProd (Anonymous,t,c) ->
-      ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
+      ope("PROD",[ast_of_pattern tenv env t;
+                  slam(None,ast_of_pattern tenv env c)])
   | PProd (na,t,c) ->
       let env' = add_name na env in
       let (n,a) =
-	factorize_binder_pattern env' 1 BProd na (ast_of_pattern env t) c in
+	factorize_binder_pattern tenv env' 1 BProd na
+          (ast_of_pattern tenv env t) c in
       (* PROD et PRODLIST doivent être distingués à cause du cas *)
       (* non dépendant, pour isoler l'implication; peut-être un *)
       (* constructeur ARROW serait-il plus justifié ? *) 
       let tag = if n=1 then "PROD" else "PRODLIST" in
-      ope(tag,[ast_of_pattern env t;a])
+      ope(tag,[ast_of_pattern tenv env t;a])
   | PLambda (na,t,c) ->
       let env' = add_name na env in
       let (n,a) =
-	factorize_binder_pattern env' 1 BLambda na (ast_of_pattern env t) c in
+	factorize_binder_pattern tenv env' 1 BLambda na
+          (ast_of_pattern tenv env t) c in
       (* LAMBDA et LAMBDALIST se comportent pareil *)
       let tag = if n=1 then "LAMBDA" else "LAMBDALIST" in
-      ope(tag,[ast_of_pattern env t;a])
+      ope(tag,[ast_of_pattern tenv env t;a])
 
   | PCase (typopt,tm,bv) ->
       warning "Old Case syntax";
-      ope("MUTCASE",(ast_of_patopt env typopt)
-	    ::(ast_of_pattern env tm)
-	    ::(Array.to_list (Array.map (ast_of_pattern env) bv)))
+      ope("MUTCASE",(ast_of_patopt tenv env typopt)
+	    ::(ast_of_pattern tenv env tm)
+	    ::(Array.to_list (Array.map (ast_of_pattern tenv env) bv)))
 
   | PSort s ->
       (match s with
@@ -395,20 +398,20 @@ let rec ast_of_pattern env = function
 
   | PMeta (Some n) -> ope("META",[num n])
   | PMeta None -> ope("ISEVAR",[])
-  | PFix f -> ast_of_raw (Detyping.detype [] env (mkFix f))
-  | PCoFix c -> ast_of_raw (Detyping.detype [] env (mkCoFix c))
+  | PFix f -> ast_of_raw (Detyping.detype tenv [] env (mkFix f))
+  | PCoFix c -> ast_of_raw (Detyping.detype tenv [] env (mkCoFix c))
 	
-and ast_of_patopt env = function
+and ast_of_patopt tenv env = function
   | None -> (string "SYNTH")
-  | Some p -> ast_of_pattern env p
+  | Some p -> ast_of_pattern tenv env p
 
-and factorize_binder_pattern env n oper na aty c =
+and factorize_binder_pattern tenv env n oper na aty c =
   let (p,body) = match decompose_binder_pattern c with
     | Some (oper',na',ty',c')
-	when (oper = oper') & (aty = ast_of_pattern env ty')
+	when (oper = oper') & (aty = ast_of_pattern tenv env ty')
 	  & not (na' = Anonymous & oper = BProd)
 	  ->
-	factorize_binder_pattern (add_name na' env) (n+1) oper na' aty c'
-    | _ -> (n,ast_of_pattern env c)
+	factorize_binder_pattern tenv (add_name na' env) (n+1) oper na' aty c'
+    | _ -> (n,ast_of_pattern tenv env c)
   in
   (p,slam(idopt_of_name na, body))
diff --git a/parsing/termast.mli b/parsing/termast.mli
index d8458263a..fb0762446 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -24,7 +24,7 @@ open Pattern
 
 val ast_of_cases_pattern : cases_pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
-val ast_of_pattern : names_context -> constr_pattern -> Coqast.t
+val ast_of_pattern : env -> names_context -> constr_pattern -> Coqast.t
 
 (* If [b=true] in [ast_of_constr b env c] then the variables in the first 
    level of quantification clashing with the variables in [env] are renamed *)
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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c6057367e..5e920ea5a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -172,7 +172,7 @@ and mk_casegoals sigma goal goalacc p c =
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
     try find_mrectype env sigma ct
-    with Induc -> anomaly "mk_casegoals" in
+    with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec pj c in
   (acc'',lbrty,conclty)
@@ -463,7 +463,7 @@ let prim_refiner r sigma goal =
             	if k = 1 then 
 		  try 
 		    let _ = find_inductive env sigma c1 in ()
-		  with Induc -> 
+		  with Not_found -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
@@ -482,7 +482,7 @@ let prim_refiner r sigma goal =
             	if k = 1 then 
 		  try 
 		    fst (find_inductive env sigma c1)
-		  with Induc -> 
+		  with Not_found -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
@@ -513,7 +513,7 @@ let prim_refiner r sigma goal =
             | _ -> 
 		try 
 		  let _ = find_coinductive env sigma b in ()
-                with Induc -> 
+                with Not_found -> 
 		  error ("All methods must construct elements " ^
 			  "in coinductive types")
 	in
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8e2a9b0ea..7c5152672 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -85,11 +85,11 @@ let get_hyps  evc = evc.it
 let get_env   evc = Global.env_of_context evc.it
 let get_gc    evc = evc.sigma
 
-let pf_lookup_name_as_renamed hyps ccl s =
-  Detyping.lookup_name_as_renamed hyps ccl s
+let pf_lookup_name_as_renamed env ccl s =
+  Detyping.lookup_name_as_renamed env ccl s
 
-let pf_lookup_index_as_renamed ccl n =
-  Detyping.lookup_index_as_renamed ccl n
+let pf_lookup_index_as_renamed env ccl n =
+  Detyping.lookup_index_as_renamed env ccl n
 
 (*********************************************************************)
 (*                  Pretty printing functions                        *)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 200adac0a..d6a1a51d5 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -42,9 +42,8 @@ val get_hyps  : named_context sigma -> named_context
 val get_env   : named_context sigma -> env
 val get_gc    : named_context sigma -> evar_map
 
-val pf_lookup_name_as_renamed : 
-  named_context -> constr -> identifier -> int option
-val pf_lookup_index_as_renamed : constr -> int -> int option
+val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
 
 (*s Pretty printing functions. *)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 6e6de2f3b..ce26640c0 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -98,7 +98,7 @@ let head_in gls indl t =
       then find_mrectype (pf_env gls) (project gls) t
       else extract_mrectype t
     in List.mem ity indl
-  with Induc -> false
+  with Not_found -> false
        
 let inductive_of_qualid gls qid =
   let c = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index aea683dc6..985db4302 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -420,7 +420,7 @@ let descend_then sigma env head dirn =
    giving [True], and all the rest giving False. *)
 
 let construct_discriminator sigma env dirn c sort =
-  let (IndType((ind,_) as indf,_) as indt) =
+  let (IndType(indf,_) as indt) =
     try find_rectype env sigma (type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
@@ -431,6 +431,7 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with 
 		 dependent types") in
+  let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = 
@@ -453,8 +454,9 @@ let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
-      let IndType ((ind,_)as indf,_) =
+      let IndType (indf,_) =
 	try find_rectype env sigma cty with Not_found -> assert false in
+      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
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2a37b3b19..5dec8457a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -373,7 +373,7 @@ let res_case_then gene thin indbinding id status gl =
   check_no_metas indclause' ccl;
   let (IndType (indf,realargs) as indt) =
     try find_rectype env sigma ccl
-    with Induc ->
+    with Not_found ->
       errorlabstrm "res_case_then"
 	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let (elim_predicate,neqns) =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4ed4f6c5..1344e009b 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -200,7 +200,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
     try find_rectype env sigma i
-    with Induc ->
+    with Not_found ->
       errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) 
   in
   let (invEnv,invGoal) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 80dad1b6b..72bf8a076 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -372,7 +372,7 @@ let dyn_intro_move = function
   | l -> bad_tactic_args "intro_move" l
 
 let rec intros_until s g =
-  match pf_lookup_name_as_renamed (pf_hyps g) (pf_concl g) s with
+  match pf_lookup_name_as_renamed (pf_env g) (pf_concl g) s with
     | Some depth -> tclDO depth intro g
     | None -> 
 	try
@@ -383,7 +383,7 @@ let rec intros_until s g =
 	      str " even after head-reduction")
 
 let rec intros_until_n_gen red n g =
-  match pf_lookup_index_as_renamed (pf_concl g) n with
+  match pf_lookup_index_as_renamed (pf_env g) (pf_concl g) n with
     | Some depth -> tclDO depth intro g
     | None ->
       if red then
@@ -1150,8 +1150,7 @@ let rec is_rec_arg env sigma indpath t =
   try
     let (ind_sp,_) = find_mrectype env sigma t in
     path_of_inductive env ind_sp = indpath
-  with Induc -> 
-    false
+  with Not_found -> false
 
 let rec recargs indpath env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with