1 files changed, 178 insertions, 316 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index abe4fcc1..d3813660 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *)
+(* $Id$ *)
 
 open Util
 open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Declarations
 open Inductiveops
 open Environ
@@ -73,11 +74,11 @@ let set_impossible_default_clause c = impossible_default_case := Some c
 let coq_unit_judge =
   let na1 = Name (id_of_string "A") in
   let na2 = Name (id_of_string "H") in
-  fun () -> 
+  fun () ->
     match !impossible_default_case with
     | Some (id,type_of_id) ->
 	make_judge id type_of_id
-    | None -> 
+    | None ->
 	(* In case the constants id/ID are not defined *)
 	make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
                  (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)))
@@ -87,8 +88,8 @@ let coq_unit_judge =
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref ->
-    type_constraint -> 
+    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
+    type_constraint ->
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
@@ -97,8 +98,8 @@ let rec list_try_compile f = function
   | [a] -> f a
   | [] -> anomaly "try_find_f"
   | h::t ->
-      try f h 
-      with UserError _ | TypeError _ | PretypeError _ 
+      try f h
+      with UserError _ | TypeError _ | PretypeError _
 	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
 	    list_try_compile f t
 
@@ -119,14 +120,11 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  list_make n (PatVar (dummy_loc,Anonymous)) 
+  list_make n (PatVar (dummy_loc,Anonymous))
 
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
 
-let push_rel_defs =
-  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
-
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
@@ -172,7 +170,7 @@ type 'a rhs =
       it         : 'a option}
 
 type 'a equation =
-    { patterns     : cases_pattern list; 
+    { patterns     : cases_pattern list;
       rhs          : 'a rhs;
       alias_stack  : name list;
       eqn_loc      : loc;
@@ -210,14 +208,12 @@ and pattern_continuation =
 
 let start_history n = Continuation (n, [], Top)
 
-let initial_history = function Continuation (_,[],Top) -> true | _ -> false
-
 let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
   | Continuation (n, _, _) ->
       anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
-  | Result _ -> 
+  | Result _ ->
       anomaly "Exhausted pattern history"
 
 (* This is for non exhaustive error message *)
@@ -248,7 +244,7 @@ let rec simplify_history = function
       let pat = match f with
 	| AliasConstructor pci ->
 	    PatCstr (dummy_loc,pci,pargs,Anonymous)
-	| AliasLeaf -> 
+	| AliasLeaf ->
 	    assert (l = []);
 	    PatVar (dummy_loc, Anonymous) in
       feed_history pat rh
@@ -266,7 +262,7 @@ let push_history_pattern n current cont =
 
   where tomatch is some sequence of "instructions" (t1  ... tn)
 
-  and mat is some matrix 
+  and mat is some matrix
    (p11 ... p1n -> rhs1)
    (    ...            )
    (pm1 ... pmn -> rhsm)
@@ -295,14 +291,14 @@ let push_history_pattern n current cont =
 
 type 'a pattern_matching_problem =
     { env       : env;
-      evdref    : evar_defs ref;
+      evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
       history   : pattern_continuation;
       mat       : 'a matrix;
       caseloc   : loc;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_defs ref -> 'a option -> unsafe_judgment }
+      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -327,7 +323,7 @@ let rec find_row_ind = function
 
 let inductive_template evdref env tmloc ind =
   let arsign = get_full_arity_sign env ind in
-  let hole_source = match tmloc with 
+  let hole_source = match tmloc with
     | Some loc -> fun i -> (loc, TomatchTypeParameter (ind,i))
     | None -> fun _ -> (dummy_loc, InternalHole) in
    let (_,evarl,_) =
@@ -337,7 +333,7 @@ let inductive_template evdref env tmloc ind =
         | None ->
 	    let ty' = substl subst ty in
 	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
-	    (e::subst,e::evarl,n+1) 
+	    (e::subst,e::evarl,n+1)
 	| Some b ->
 	    (b::subst,evarl,n+1))
       arsign ([],[],1) in
@@ -354,7 +350,7 @@ let try_find_ind env sigma typ realnames =
 
 let inh_coerce_to_ind evdref env ty tyi =
   let expected_typ = inductive_template evdref env None tyi in
-     (* devrait être indifférent d'exiger leq ou pas puisque pour 
+     (* devrait être indifférent d'exiger leq ou pas puisque pour
         un inductif cela doit être égal *)
   let _ = e_cumul env evdref expected_typ ty in ()
 
@@ -363,23 +359,23 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
 	inh_coerce_to_ind evdref env typ ind;
-	try try_find_ind env (evars_of !evdref) typ realnames
+	try try_find_ind env !evdref typ realnames
 	with Not_found -> NotInd (None,typ)
 
 let find_tomatch_tycon evdref env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_,realnal) -> 		  
+  | Some (_,ind,_,realnal) ->
       mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal)
-  | None -> 
+  | None ->
       empty_tycon,None
 
 let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_rawconstr tomatch) in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
-  let typ = nf_evar (evars_of !evdref) j.uj_type in
+  let typ = nf_evar !evdref j.uj_type in
   let t =
-    try try_find_ind env (evars_of !evdref) typ realnames
+    try try_find_ind env !evdref typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
@@ -409,12 +405,12 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
   (* In practice, we coerce the term to match if it is not already an
-     inductive type and it is not dependent; moreover, we use only 
+     inductive type and it is not dependent; moreover, we use only
      the first pattern type and forget about the others *)
   let typ,names =
     match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
   let typ =
-    try try_find_ind pb.env (evars_of !(pb.evdref)) typ names
+    try try_find_ind pb.env !(pb.evdref) typ names
     with Not_found -> NotInd (None,typ) in
   let tomatch = ((current,typ),deps,dep) in
   match typ with
@@ -432,7 +428,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
 		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
-	    let sigma = evars_of !(pb.evdref) in
+	    let sigma =  !(pb.evdref) in
 	    let typ = try_find_ind pb.env sigma indt names in
 	    ((current,typ),deps,dep))
   | _ -> tomatch
@@ -452,9 +448,6 @@ let map_tomatch_type f = function
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
 
-let lift_tomatch n ((current,typ),info) =
-  ((lift n current,lift_tomatch_type n typ),info)
-
 (**********************************************************************)
 (* Utilities on patterns *)
 
@@ -467,12 +460,6 @@ let alias_of_pat = function
   | PatVar (_,name) -> name
   | PatCstr(_,_,_,name) -> name
 
-let unalias_pat = function
-  | PatVar (c,name) as p ->
-      if name = Anonymous then p else PatVar (c,Anonymous)
-  | PatCstr(a,b,c,name) as p ->
-      if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
-
 let remove_current_pattern eqn =
   match eqn.patterns with
     | pat::pats ->
@@ -497,18 +484,18 @@ let rec adjust_local_defs loc = function
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor env ind cstrs = function 
+let check_and_adjust_constructor env ind cstrs = function
   | PatVar _ as pat -> pat
   | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
-      if Closure.mind_equiv env ind' ind then
+      if eq_ind ind' ind then
 	(* Check the constructor has the right number of args *)
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
 	if List.length args = nb_args_constr then pat
 	else
-	  try 
+	  try
 	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
 	    in PatCstr (loc, cstr, args', alias)
 	  with NotAdjustable ->
@@ -518,7 +505,7 @@ let check_and_adjust_constructor env ind cstrs = function
 	(* Try to insert a coercion *)
 	try
 	  Coercion.inh_pattern_coerce_to loc pat ind' ind
-	with Not_found -> 
+	with Not_found ->
 	  error_bad_constructor_loc loc cstr ind
 
 let check_all_variables typ mat =
@@ -530,14 +517,14 @@ let check_all_variables typ mat =
     mat
 
 let check_unused_pattern env eqn =
-  if not !(eqn.used) then 
+  if not !(eqn.used) then
     raise_pattern_matching_error
       (eqn.eqn_loc, env, UnusedClause eqn.patterns)
 
 let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
-  match pb.mat with 
+  match pb.mat with
     | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
@@ -588,7 +575,7 @@ let dependencies_in_rhs nargs current tms eqns =
 
 let rec find_dependency_list k n = function
   | [] -> []
-  | (used,tdeps,d)::rest -> 
+  | (used,tdeps,d)::rest ->
       let deps = find_dependency_list k (n+1) rest in
       if used && dependent_decl (mkRel n) d
       then list_add_set (List.length rest + 1) (list_union deps tdeps)
@@ -615,7 +602,7 @@ let find_dependencies_signature deps_in_rhs typs =
 
 let regeneralize_index_tomatch n =
   let rec genrec depth = function
-  | [] -> 
+  | [] ->
       []
   | Pushed ((c,tm),l,dep) :: rest ->
       let c = regeneralize_index n depth c in
@@ -629,7 +616,7 @@ let regeneralize_index_tomatch n =
       :: genrec (depth+1) rest in
   genrec 0
 
-let rec replace_term n c k t = 
+let rec replace_term n c k t =
   if t = mkRel (n+k) then lift k c
   else map_constr_with_binders succ (replace_term n c) k t
 
@@ -652,9 +639,6 @@ let replace_tomatch n c =
       :: replrec (depth+1) rest in
   replrec 0
 
-let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
-let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
-
 (* [liftn_tomatch_stack]: a term to match has just been substituted by
    some constructor t = (ci x1...xn) and the terms x1 ... xn have been
    added to match; all pushed terms to match must be lifted by n
@@ -690,7 +674,7 @@ let lift_tomatch_stack n = liftn_tomatch_stack n 1
    [match y with (S (S x)) => x | x => x end] should be compiled into
    [match y with O => y | (S n) => match n with O => y | (S x) => x end end]
 
-   and [match y with (S (S n)) => n | n => n end] into 
+   and [match y with (S (S n)) => n | n => n end] into
    [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
 
   i.e. user names should be preserved and created names should not
@@ -705,7 +689,7 @@ let merge_names get_name = List.map2 (merge_name get_name)
 let get_names env sign eqns =
   let names1 = list_make (List.length sign) Anonymous in
   (* If any, we prefer names used in pats, from top to bottom *)
-  let names2 = 
+  let names2 =
     List.fold_right
       (fun (pats,eqn) names -> merge_names alias_of_pat pats names)
       eqns names1 in
@@ -719,7 +703,7 @@ let get_names env sign eqns =
 	 let na =
 	   merge_name
 	     (fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid))
-	     d na 
+	     d na
 	 in
          (na::l,(out_name na)::avoid))
       ([],allvars) (List.rev sign) names2 in
@@ -756,7 +740,7 @@ let build_aliases_context env sigma names allpats pats =
 	let oldallpats = List.map List.tl oldallpats in
 	let decl = (na,Some deppat,t) in
 	let a = (deppat,nondeppat,d,t) in
-	insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) 
+	insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
 	  newallpats oldallpats (pats,names)
     | [], [] -> newallpats, sign1, sign2, env
     | _ -> anomaly "Inconsistent alias and name lists" in
@@ -776,7 +760,7 @@ let insert_aliases env sigma alias eqns =
   let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
   let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
   (* name2 takes the meet of all needed aliases *)
-  let name2 = 
+  let name2 =
     List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in
   (* Only needed aliases are kept by build_aliases_context *)
   let eqnsnames, sign1, sign2, env =
@@ -793,7 +777,7 @@ let noccur_between_without_evar n m term =
     | Rel p       -> if n<=p && p<n+m then raise Occur
     | Evar (_,cl) -> ()
     | _             -> iter_constr_with_binders succ occur_rec n c
-  in 
+  in
   (m = 0) or (try occur_rec n term; true with Occur -> false)
 
 
@@ -870,7 +854,7 @@ let subst_predicate (args,copt) ccl tms =
 
 let specialize_predicate_var (cur,typ,dep) tms ccl =
   let c = if dep<>Anonymous then Some cur else None in
-  let l = 
+  let l =
     match typ with
     | IsInd (_,IndType(_,realargs),names) -> if names<>[] then realargs else []
     | NotInd _ -> [] in
@@ -918,7 +902,7 @@ let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
       | Rel i -> regeneralize_index_tomatch (i+n) tms
       | _ -> (* Initial case *) tms in
   let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (nadep::names) sign in
-  let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in 
+  let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in
   let pred = extract_predicate [] ccl tms in
   it_mkLambda_or_LetIn_name env pred sign
 
@@ -930,24 +914,24 @@ let known_dependent (_,dep) = (dep = KnownDep)
    by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *)
 
 let expand_arg tms ccl ((_,t),_,na) =
-  let k = length_of_tomatch_type_sign na t in 
+  let k = length_of_tomatch_type_sign na t in
   lift_predicate (k-1) ccl tms
 
 let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
-    match kind_of_term (whd_evar (evars_of !(pb.evdref)) pred) with
+    match kind_of_term (whd_evar !(pb.evdref) pred) with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase ->
 	let default = (coq_unit_judge ()).uj_type in
-	pb.evdref := Evd.evar_define evk default !(pb.evdref);
+	pb.evdref := Evd.define evk default !(pb.evdref);
       (* we add an "assert false" case *)
       let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in
       let aliasnames =
 	map_succeed (function Alias _ -> Anonymous | _ -> failwith"") tomatch
       in
       [ { patterns = pats;
-          rhs = { rhs_env = pb.env; 
-	          rhs_vars = []; 
-		  avoid_ids = []; 
+          rhs = { rhs_env = pb.env;
+	          rhs_vars = [];
+		  avoid_ids = [];
 		  it = None };
 	  alias_stack = Anonymous::aliasnames;
 	  eqn_loc = dummy_loc;
@@ -971,14 +955,18 @@ let adjust_impossible_cases pb pred tomatch submat =
 (* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
 (*                                                                           *)
 (*****************************************************************************)
-let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
+let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
   (* Assume some gamma st: gamma, (X,x:=realargs,copt), tms |- ccl *)
   let nrealargs = List.length names in
   let k = nrealargs + (if depna<>Anonymous then 1 else 0) in
   (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt), tms |- ccl' *)
   let n = cs.cs_nargs in
   let ccl' = liftn_predicate n (k+1) ccl tms in
-  let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
+  let argsi =
+    if nrealargs <> 0 then
+      adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs)
+    else
+      [] in
   let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
   (* The substituends argsi, copti are all defined in gamma, x1...xn *)
   (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
@@ -990,8 +978,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
   List.fold_left (expand_arg tms) ccl''' newtomatchs
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in
-  (pred, whd_betaiota (evars_of !evdref)
+  let pred= abstract_predicate env !evdref indf current dep tms p in
+  (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])), new_Type ())
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
@@ -1037,8 +1025,8 @@ let group_equations pb ind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor pb.env ind cstrs pat with 
-	   | PatVar (_,name) -> 
+	 match check_and_adjust_constructor pb.env ind cstrs pat with
+	   | PatVar (_,name) ->
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
 		 let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
@@ -1058,6 +1046,7 @@ let rec generalize_problem names pb = function
   | [] -> pb
   | i::l ->
       let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+      let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *)
       let pb' = generalize_problem names pb l in
       let tomatch = lift_tomatch_stack 1 pb'.tomatch in
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
@@ -1069,7 +1058,7 @@ let rec generalize_problem names pb = function
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
-  j_nf_evar (evars_of !(pb.evdref)) j
+  j_nf_evar !(pb.evdref) j
 
 (* Building the sub-problem when all patterns are variables *)
 let shift_problem ((current,t),_,(nadep,_)) pb =
@@ -1080,17 +1069,17 @@ let shift_problem ((current,t),_,(nadep,_)) pb =
      mat = List.map remove_current_pattern pb.mat }
 
 (* Building the sub-pattern-matching problem for a given branch *)
-let build_branch current deps (realnames,dep) pb eqns const_info =
+let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   (* We remember that we descend through a constructor *)
   let alias_type =
     if Array.length const_info.cs_concl_realargs = 0
       & not (known_dependent dep) & deps = []
     then
       NonDepAlias
-    else 
+    else
       DepAlias
   in
-  let history = 
+  let history =
     push_history_pattern const_info.cs_nargs
       (AliasConstructor const_info.cs_cstr)
       pb.history in
@@ -1109,10 +1098,10 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
 
   let dep_sign =
     find_dependencies_signature
-      (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns) 
+      (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns)
       (List.rev typs) in
 
-  (* The dependent term to subst in the types of the remaining UnPushed 
+  (* The dependent term to subst in the types of the remaining UnPushed
      terms is relative to the current context enriched by topushs *)
   let ci = build_dependent_constructor const_info in
 
@@ -1125,7 +1114,7 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
   let pred_is_not_dep =
     noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
 
-  let typs'' = 
+  let typs'' =
     list_map2_i
       (fun i (na,t) deps ->
 	let dep = match dep with
@@ -1139,8 +1128,8 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
 	((mkRel i, lift_tomatch_type i t),deps,dep))
       1 typs' (List.rev dep_sign) in
 
-  let pred = 
-    specialize_predicate typs'' (realnames,dep) const_info tomatch pb.pred in
+  let pred =
+    specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in
 
   let currents = List.map (fun x -> Pushed x) typs'' in
 
@@ -1199,6 +1188,7 @@ and match_current pb tomatch =
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
 	let cstrs = get_constructors pb.env indf in
+	let arsign, _ = get_arity pb.env indf in
 	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
 	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
 	  compile (shift_problem ct pb)
@@ -1209,12 +1199,12 @@ and match_current pb tomatch =
 	  let pb = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brs = array_map2 (compile_branch current (names,dep) deps pb) eqns cstrs in
+	  let brs = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in
 
 	  (* We build the (elementary) case analysis *)
 	  let brvals = Array.map (fun (v,_) -> v) brs in
 	  let (pred,typ,s) =
-	    find_predicate pb.caseloc pb.env pb.evdref 
+	    find_predicate pb.caseloc pb.env pb.evdref
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
 	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
@@ -1222,8 +1212,8 @@ and match_current pb tomatch =
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
 
-and compile_branch current names deps pb eqn cstr =
-  let sign, pb = build_branch current deps names pb eqn cstr in
+and compile_branch current names deps pb arsign eqn cstr =
+  let sign, pb = build_branch current deps names pb arsign eqn cstr in
   let j = compile pb in
   (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
 
@@ -1240,7 +1230,7 @@ and compile_generalization pb d rest =
 and compile_alias pb (deppat,nondeppat,d,t) rest =
   let history = simplify_history pb.history in
   let sign, newenv, mat =
-    insert_aliases pb.env (evars_of !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in
+    insert_aliases pb.env !(pb.evdref) (deppat,nondeppat,d,t) pb.mat in
   let n = List.length sign in
 
   (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
@@ -1287,102 +1277,6 @@ let matx_of_eqns env tomatchl eqns =
       rhs = rhs }
   in List.map build_eqn eqns
 
-(************************************************************************)
-(* preparing the elimination predicate if any                          *)
-
-let build_expected_arity env evdref isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_),_) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args),_) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),_,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),_,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs),_))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 (***************** Building an inversion predicate ************************)
 
 (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T"
@@ -1395,9 +1289,9 @@ let set_arity_signature dep n arsign tomatchl pred x =
    variables (in practice, there is no reason that ti is already
    constructed and the qi will be degenerated).
 
-   We then look for a type U(..a1jk..b1 .. ..amjk..bm) so that 
+   We then look for a type U(..a1jk..b1 .. ..amjk..bm) so that
    T = U(..v1jk..t1 .. ..vmjk..tm). This a higher-order matching
-   problem with a priori different solution (one of them if T itself!).
+   problem with a priori different solutions (one of them if T itself!).
 
    We finally invert the uij and the ti and build the return clause
 
@@ -1414,27 +1308,27 @@ let set_arity_signature dep n arsign tomatchl pred x =
 let adjust_to_extended_env_and_remove_deps env extenv subst t =
   let n = rel_context_length (rel_context env) in
   let n' = rel_context_length (rel_context extenv) in
-  (* We first remove the bindings that are dependently typed (they are 
+  (* We first remove the bindings that are dependently typed (they are
      difficult to manage and it is not sure these are so useful in practice);
      Notes:
      - [subst] is made of pairs [(id,u)] where id is a name in [extenv] and
        [u] a term typed in [env];
      - [subst0] is made of items [(p,u,(u,ty))] where [ty] is the type of [u]
-       and both are adjusted to [extenv] while [p] is the index of [id] in 
+       and both are adjusted to [extenv] while [p] is the index of [id] in
        [extenv] (after expansion of the aliases) *)
   let subst0 = map_succeed (fun (x,u) ->
     (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
-    let (p,_) = lookup_rel_id x (rel_context extenv) in
+    let (p,_,_) = lookup_rel_id x (rel_context extenv) in
     let rec aux n (_,b,ty) =
       match b with
       | Some c ->
 	  assert (isRel c);
-	  let p = n + destRel c in aux p (lookup_rel p (rel_context extenv))
+	  let p = n + destRel c in aux p (lookup_rel p extenv)
       | None ->
 	  (n,ty) in
-    let (p,ty) = aux p (lookup_rel p (rel_context extenv)) in
+    let (p,ty) = aux p (lookup_rel p extenv) in
     if noccur_between_without_evar 1 (n'-p-n+1) ty
     then
       let u = lift (n'-n) u in
@@ -1444,12 +1338,15 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
   let t0 = lift (n'-n) t in
   (subst0,t0)
 
+let push_binder d (k,env,subst) =
+  (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+
 (* Let vijk and ti be a set of dependent terms and T a type, all
  * defined in some environment env. The vijk and ti are supposed to be
  * instances for variables aijk and bi.
  *
- * [abstract_tycon Gamma0 Sigma subst T Gamma] looks for U(..v1jk..t1 .. ..vmjk..tm) 
- * defined in some extended context 
+ * [abstract_tycon Gamma0 Sigma subst T Gamma] looks for U(..v1jk..t1 .. ..vmjk..tm)
+ * defined in some extended context
  * "Gamma0, ..a1jk:V1jk.. b1:W1 .. ..amjk:Vmjk.. bm:Wm"
  * such that env |- T = U(..v1jk..t1 .. ..vmjk..tm). To not commit to
  * a particular solution, we replace each subterm t in T that unifies with
@@ -1460,7 +1357,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
 *)
 
 let abstract_tycon loc env evdref subst _tycon extenv t =
-  let sigma = evars_of !evdref in
+  let sigma = !evdref in
   let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
@@ -1469,15 +1366,18 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
      by an evar that may depend (and only depend) on the corresponding
      convertible subterms of the substitution *)
   let rec aux (k,env,subst as x) t =
+    if isRel t && pi2 (lookup_rel (destRel t) env) <> None then
+      map_constr_with_full_binders push_binder aux x t
+    else
     let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
     if good <> [] then
       let (u,ty) = pi3 (List.hd good) in
       let vl = List.map pi1 good in
-      let inst = 
+      let inst =
 	list_map_i
 	  (fun i _ -> if List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
-      let rel_filter = 
+      let rel_filter =
 	List.map (fun a -> not (isRel a) or dependent a u) inst in
       let named_filter =
 	List.map (fun (id,_,_) -> dependent (mkVar id) u)
@@ -1488,30 +1388,25 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       evdref := add_conv_pb (Reduction.CONV,extenv,substl inst ev,u) !evdref;
       lift k ev
     else
-      map_constr_with_full_binders 
-	(fun d (k,env,subst) ->
-	  k+1,
-	  push_rel d env, 
-	  List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
-	aux x t in
+      map_constr_with_full_binders push_binder aux x t in
   aux (0,extenv,subst0) t0
 
 let build_tycon loc env tycon_env subst tycon extenv evdref t =
   let t = match t with
     | None ->
-	(* This is the situation we are building a return predicate and 
+	(* This is the situation we are building a return predicate and
            we are in an impossible branch *)
 	let n = rel_context_length (rel_context env) in
 	let n' = rel_context_length (rel_context tycon_env) in
-	let impossible_case_type = 
+	let impossible_case_type =
 	  e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in
 	lift (n'-n) impossible_case_type
     | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in
-  get_judgment_of extenv (evars_of !evdref) t
+  get_judgment_of extenv !evdref t
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
- * predicate for Xi that is itself made by an auxiliary 
+ * predicate for Xi that is itself made by an auxiliary
  * pattern-matching problem of which the first clause reveals the
  * pattern structure of the constraints on the inductive types of the t1..tn,
  * and the second clause is a wildcard clause for catching the
@@ -1519,8 +1414,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
  * further explanations
  *)
 
-let build_inversion_problem loc env evdref tms t =
-  let sigma = evars_of !evdref in
+let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env t Anonymous) avoid in
     PatVar (dummy_loc,Name id), ((id,t)::subst, id::avoid) in
@@ -1596,12 +1490,13 @@ let build_inversion_problem loc env evdref tms t =
       alias_stack = [];
       eqn_loc = dummy_loc;
       used = ref false;
-      rhs = { rhs_env = pb_env; 
-              rhs_vars = []; 
+      rhs = { rhs_env = pb_env;
+              rhs_vars = [];
 	      avoid_ids = avoid0;
 	      it = None } } in
-  (* [pb] is the auxiliary pattern-matching serving as skeleton for the 
+  (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
+  let evdref = ref sigma in
   let pb =
     { env       = pb_env;
       evdref    = evdref;
@@ -1612,26 +1507,9 @@ let build_inversion_problem loc env evdref tms t =
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon loc env pb_env subst} in
-  (compile pb).uj_val
+  let pred = (compile pb).uj_val in
+  (!evdref,pred)
 
-let prepare_predicate_from_tycon loc dep env evdref tomatchs sign c =
-  let cook (n, l, env, signs) = function
-    | c,IsInd (_,IndType(indf,realargs),_) ->
-	let indf' = lift_inductive_family n indf in
-	let sign = make_arity_signature env dep indf' in
-	let p = List.length realargs in
-	if dep then
-	  (n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs)
-	else
-	  (n + p, (List.rev realargs)@l, push_rels sign env,sign::signs)
-    | c,NotInd (bo,typ) ->
-	let sign = [Anonymous,Option.map (lift n) bo,lift n typ] in
-	let sign = name_context env sign in
-	(n + 1, c::l, push_rels sign env, sign::signs) in
-  let n,allargs,env',signs = List.fold_left cook (0, [], env, []) tomatchs in
-  let names = List.rev (List.map (List.map pi1) signs) in
-  names, build_inversion_problem loc env evdref tomatchs c
-  
 (* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
 let build_initial_predicate knowndep allnames pred =
@@ -1658,27 +1536,27 @@ let build_initial_predicate knowndep allnames pred =
 let extract_arity_signature env0 tomatchl tmsign =
   let get_one_sign n tm (na,t) =
     match tm with
-      | NotInd (bo,typ) -> 
+      | NotInd (bo,typ) ->
 	  (match t with
 	    | None -> [na,Option.map (lift n) bo,lift n typ]
-	    | Some (loc,_,_,_) -> 
+	    | Some (loc,_,_,_) ->
  	    user_err_loc (loc,"",
 	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
-	  let (ind,params) = dest_ind_family indf' in
-	  let nrealargs = List.length realargs in
+	  let (ind,_) = dest_ind_family indf' in
+	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs env0 ind in
+	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type.");
-		  if List.length params <> nparams
-		    or nrealargs <> List.length realnal then
+		  if nparams_ctxt <> nparams
+		    or nrealargs_ctxt <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
-	      | None -> list_make nrealargs Anonymous in
-	  let arsign = fst (get_arity env0 indf') in
+	      | None -> list_make nrealargs_ctxt Anonymous in
 (* 	  let na =  *)
 (* 	    match na with  *)
 (* 	      | Name _ -> na *)
@@ -1707,43 +1585,46 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c =
+let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
-  let subst, len = 
+  let subst, len =
     List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel n when dependent tm c 
+	  | Rel n when dependent tm c
 		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
 	      ((n, len) :: subst, len - signlen)
-	  | Rel _ when not (dependent tm c)
-		&& signlen > 1 (* The term is of a dependent type but does not appear in 
-				  the tycon, maybe some variable in its type does. *) ->
+	  | Rel n when signlen > 1 (* The term is of a dependent type,
+				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
 		| IsInd (_, IndType(indf,realargs),_) ->
-		    List.fold_left
-		      (fun (subst, len) arg -> 
-			match kind_of_term arg with
+		    let subst =
+		      if dependent tm c && List.for_all isRel realargs
+		      then (n, 1) :: subst else subst
+		    in
+		      List.fold_left
+			(fun (subst, len) arg ->
+			  match kind_of_term arg with
 			  | Rel n when dependent arg c ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
-		      (subst, len) realargs)
+			(subst, len) realargs)
 	  | _ -> (subst, len - signlen))
       ([], nar) tomatchs arsign
   in
   let rec predicate lift c =
     match kind_of_term c with
-      | Rel n when n > lift -> 
-	  (try 
+      | Rel n when n > lift ->
+	  (try
 	      (* Make the predicate dependent on the matched variable *)
 	      let idx = List.assoc (n - lift) subst in
 		mkRel (idx + lift)
-	    with Not_found -> 
+	    with Not_found ->
 	      (* A variable that is not matched, lift over the arsign. *)
 	      mkRel (n + nar))
       | _ ->
-	  map_constr_with_binders succ predicate lift c 
+	  map_constr_with_binders succ predicate lift c
   in predicate 0 c
 
 
@@ -1758,92 +1639,71 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let is_dependent_on_rel x t =
-  match kind_of_term x with
-      Rel n -> not (noccur_with_meta n n t)
-    | _ -> false
-
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
-  match pred with
-  (* No type annotation *)
-  | None ->
-      (match tycon with
-       | Some (None, t) when not (noccur_with_meta 0 max_int t) ->
-	   (* If the tycon is not closed w.r.t real variables *)
-	   (* We try two different strategies *)
-	   let evdref2 = ref !evdref in
-           let arsign = extract_arity_signature env tomatchs sign in
-           let env' = List.fold_right push_rels arsign env in
-	   (* First strategy: we abstract the tycon wrt to the dependencies *)
-           let names1 = List.rev (List.map (List.map pi1) arsign) in
-           let pred1 = prepare_predicate_from_arsign_tycon loc env' tomatchs sign arsign t in
-           let nal1,pred1 = build_initial_predicate KnownDep names1 pred1 in
-	   (* Second strategy: we build an "inversion" predicate *)
-	   let names2,pred2 = 
-	     prepare_predicate_from_tycon loc true env evdref2 tomatchs sign t
-	   in 
-	   let nal2,pred2 = build_initial_predicate DepUnknown names2 pred2 in
-	   [evdref, nal1, pred1; evdref2, nal2, pred2]
-       | Some (None, t) ->
-	   (* Only one strategy: we build an "inversion" predicate *)
-	   let names,pred = 
-	     prepare_predicate_from_tycon loc true env evdref tomatchs sign t
-	   in 
-	   let nal,pred = build_initial_predicate DepUnknown names pred in
-	   [evdref, nal, pred]
-       | _ ->
-	   (* No type constaints: we use two strategies *)
-	   let evdref2 = ref !evdref in
-	   let t1 = mkExistential env ~src:(loc, CasesType) evdref in
-	   (* First strategy: we pose a possibly dependent "inversion" evar *)
-	   let names1,pred1 = 
-	     prepare_predicate_from_tycon loc true env evdref tomatchs sign t1
-	   in 
-	   let nal1,pred1 = build_initial_predicate DepUnknown names1 pred1 in
-	   (* Second strategy: we pose a non dependent evar *)
-	   let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in
-           let arsign = extract_arity_signature env tomatchs sign in
-           let names2 = List.rev (List.map (List.map pi1) arsign) in
-           let pred2 = lift (List.length names2) t2 in
-	   let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in
-	   [evdref, nal1, pred1; evdref2, nal2, pred2])
-
-  (* Some type annotation *)
-  | Some rtntyp ->
+  let arsign = extract_arity_signature env tomatchs sign in
+  let names = List.rev (List.map (List.map pi1) arsign) in
+  let preds =
+    match pred, tycon with
+    (* No type annotation *)
+    | None, Some (None, t) when not (noccur_with_meta 0 max_int t) ->
+	(* If the tycon is not closed w.r.t real variables, we try *)
+        (* two different strategies *)
+	(* First strategy: we abstract the tycon wrt to the dependencies *)
+        let pred1 =
+          prepare_predicate_from_arsign_tycon loc tomatchs sign arsign t in
+	(* Second strategy: we build an "inversion" predicate *)
+	let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in
+	[!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2]
+    | None, Some (None, t) ->
+	(* Only one strategy: we build an "inversion" predicate *)
+	let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in
+	[sigma, DepUnknown, pred]
+    | None,  _ ->
+	(* No type constaints: we use two strategies *)
+	let t = mkExistential env ~src:(loc, CasesType) evdref in
+	(* First strategy: we build an inversion problem *)
+	let sigma1,pred1 = build_inversion_problem loc env !evdref tomatchs t in
+	(* Second strategy: we directly use the evar as a non dependent pred *)
+        let pred2 = lift (List.length names) t in
+	[sigma1, DepUnknown, pred1; !evdref, KnownNotDep, pred2]
+    (* Some type annotation *)
+    | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
-      let arsign = extract_arity_signature env tomatchs sign in
       let env = List.fold_right push_rels arsign env in
-      let allnames = List.rev (List.map (List.map pi1) arsign) in
       let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in
-      let _ = 
-	Option.map (fun tycon -> 
-		      evdref := Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val 
-		      (lift_tycon_type (List.length arsign) tycon))
-	  tycon
-      in
-      let predccl = (j_nf_isevar !evdref predcclj).uj_val in      
-      let nal,pred = build_initial_predicate KnownDep allnames predccl in
-      [evdref, nal, pred]
+      Option.iter (fun tycon ->
+          let tycon = lift_tycon_type (List.length arsign) tycon in
+	  evdref :=
+            Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
+        tycon;
+      let predccl = (j_nf_evar !evdref predcclj).uj_val in
+      [!evdref, KnownDep, predccl]
+  in
+  List.map
+    (fun (sigma,dep,pred) ->
+      let (nal,pred) = build_initial_predicate dep names pred in
+      sigma,nal,pred)
+    preds
 
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
-  
+
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
 
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env tomatchl eqns in
-    
+
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
   let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
-    
+
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
   let sign = List.map snd tomatchl in
   let preds = prepare_predicate loc typing_fun evdref env tomatchs sign tycon predopt in
-    
-  let compile_for_one_predicate (myevdref,nal,pred) =
+
+  let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
     (* names of aliases will be recovered from patterns (hence Anonymous *)
     (* here) *)
@@ -1854,6 +1714,8 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     | Some t ->	typing_fun tycon env evdref t
     | None -> coq_unit_judge () in
 
+    let myevdref = ref sigma in
+
     let pb =
       { env       = env;
         evdref    = myevdref;