Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 615 insertions, 494 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 749101f7..8963ea5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *)
-
+open Compat
 open Util
 open Names
 open Nameops
@@ -21,7 +20,7 @@ open Sign
 open Reductionops
 open Typeops
 open Type_errors
-open Rawterm
+open Glob_term
 open Retyping
 open Pretype_errors
 open Evarutil
@@ -44,7 +43,7 @@ type pattern_matching_error =
 exception PatternMatchingError of env * pattern_matching_error
 
 let raise_pattern_matching_error (loc,ctx,te) =
-  Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te))
+  Loc.raise loc (PatternMatchingError(ctx,te))
 
 let error_bad_pattern_loc loc cstr ind =
   raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
@@ -64,33 +63,12 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 =
 let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
-(**********************************************************************)
-(* Functions to deal with impossible cases *)
-
-let impossible_default_case = ref None
-
-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 () ->
-    match !impossible_default_case with
-    | Some (id,type_of_id) ->
-	make_judge id type_of_id
-    | 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)))
-
-(**********************************************************************)
-
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
+    (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
-    env -> rawconstr option * tomatch_tuples * cases_clauses ->
+    env -> glob_constr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
@@ -100,7 +78,7 @@ let rec list_try_compile f = function
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _
-	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+	| Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
 	    list_try_compile f t
 
 let force_name =
@@ -128,37 +106,13 @@ let push_rels vars env = List.fold_right push_rel vars env
 (* 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'] *)
 
-let regeneralize_rel i k j = if j = i+k then k+1 else j
-
-let rec regeneralize_index i k t = match kind_of_term t with
-  | Rel j when j = i+k -> mkRel (k+1)
-  | Rel j when j < i+k -> t
-  | Rel j when j > i+k -> t
-  | _ -> map_constr_with_binders succ (regeneralize_index i) k t
+let relocate_rel n1 n2 k j = if j = n1+k then n2+k else j
 
-type alias_constr =
-  | DepAlias
-  | NonDepAlias
-
-let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
-  { uj_val =
-    if
-      isRel deppat or not (dependent (mkRel 1) j.uj_val) or
-      d = NonDepAlias & not (dependent (mkRel 1) j.uj_type)
-    then
-      (* The body of pat is not needed to type j - see *)
-      (* insert_aliases - and both deppat and nondeppat have the *)
-      (* same type, then one can freely substitute one by the other. *)
-      (* We use nondeppat only if it's a Rel to preserve sharing. *)
-      if isRel nondeppat then
-        subst1 nondeppat j.uj_val
-      else subst1 deppat j.uj_val
-    else
-      (* The body of pat is not needed to type j but its value *)
-      (* is dependent in the type of j; our choice is to *)
-      (* enforce this dependency *)
-      mkLetIn (na,deppat,t,j.uj_val);
-    uj_type = subst1 deppat j.uj_type }
+let rec relocate_index n1 n2 k t = match kind_of_term t with
+  | Rel j when j = n1+k -> mkRel (n2+k)
+  | Rel j when j < n1+k -> t
+  | Rel j when j > n1+k -> t
+  | _ -> map_constr_with_binders succ (relocate_index n1 n2) k t
 
 (**********************************************************************)
 (* Structures used in compiling pattern-matching *)
@@ -178,29 +132,24 @@ type 'a equation =
 
 type 'a matrix = 'a equation list
 
-type dep_status = KnownDep | KnownNotDep | DepUnknown
-
 (* 1st argument of IsInd is the original ind before extracting the summary *)
 type tomatch_type =
   | IsInd of types * inductive_type * name list
   | NotInd of constr option * types
 
 type tomatch_status =
-  | Pushed of ((constr * tomatch_type) * int list * (name * dep_status))
-  | Alias of (constr * constr * alias_constr * constr)
-  | Abstract of rel_declaration
+  | Pushed of ((constr * tomatch_type) * int list * name)
+  | Alias of (name * constr * (constr * types))
+  | NonDepAlias
+  | Abstract of int * rel_declaration
 
 type tomatch_stack = tomatch_status list
 
 (* We keep a constr for aliases and a cases_pattern for error message *)
 
-type alias_builder =
-  | AliasLeaf
-  | AliasConstructor of constructor
-
 type pattern_history =
   | Top
-  | MakeAlias of alias_builder * pattern_continuation
+  | MakeConstructor of constructor * pattern_continuation
 
 and pattern_continuation =
   | Continuation of int * cases_pattern list * pattern_history
@@ -218,51 +167,47 @@ let feed_history arg = function
 
 (* This is for non exhaustive error message *)
 
-let rec rawpattern_of_partial_history args2 = function
+let rec glob_pattern_of_partial_history args2 = function
   | Continuation (n, args1, h) ->
       let args3 = make_anonymous_patvars (n - (List.length args2)) in
-      build_rawpattern (List.rev_append args1 (args2@args3)) h
+      build_glob_pattern (List.rev_append args1 (args2@args3)) h
   | Result pl -> pl
 
-and build_rawpattern args = function
+and build_glob_pattern args = function
   | Top -> args
-  | MakeAlias (AliasLeaf, rh) ->
-      assert (args = []);
-      rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
-  | MakeAlias (AliasConstructor pci, rh) ->
-      rawpattern_of_partial_history
+  | MakeConstructor (pci, rh) ->
+      glob_pattern_of_partial_history
 	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
 
-let complete_history = rawpattern_of_partial_history []
+let complete_history = glob_pattern_of_partial_history []
 
 (* This is to build glued pattern-matching history and alias bodies *)
 
-let rec simplify_history = function
-  | Continuation (0, l, Top) -> Result (List.rev l)
-  | Continuation (0, l, MakeAlias (f, rh)) ->
-      let pargs = List.rev l in
-      let pat = match f with
-	| AliasConstructor pci ->
-	    PatCstr (dummy_loc,pci,pargs,Anonymous)
-	| AliasLeaf ->
-	    assert (l = []);
-	    PatVar (dummy_loc, Anonymous) in
-      feed_history pat rh
-  | h -> h
+let rec pop_history_pattern = function
+  | Continuation (0, l, Top) ->
+      Result (List.rev l)
+  | Continuation (0, l, MakeConstructor (pci, rh)) ->
+      feed_history (PatCstr (dummy_loc,pci,List.rev l,Anonymous)) rh
+  | _ ->
+      anomaly "Constructor not yet filled with its arguments"
+
+let pop_history h =
+  feed_history (PatVar (dummy_loc, Anonymous)) h
 
 (* Builds a continuation expecting [n] arguments and building [ci] applied
    to this [n] arguments *)
 
-let push_history_pattern n current cont =
-  Continuation (n, [], MakeAlias (current, cont))
+let push_history_pattern n pci cont =
+  Continuation (n, [], MakeConstructor (pci, cont))
 
 (* A pattern-matching problem has the following form:
 
-   env, evd |- <pred> Cases tomatch of mat end
+   env, evd |- match terms_to_tomatch return pred with mat end
 
-  where tomatch is some sequence of "instructions" (t1  ... tn)
+  where terms_to_match is some sequence of "instructions" (t1 ... tp)
 
   and mat is some matrix
+
    (p11 ... p1n -> rhs1)
    (    ...            )
    (pm1 ... pmn -> rhsm)
@@ -270,16 +215,25 @@ let push_history_pattern n current cont =
   Terms to match: there are 3 kinds of instructions
 
   - "Pushed" terms to match are typed in [env]; these are usually just
-    Rel(n) except for the initial terms given by user and typed in [env]
-  - "Abstract" instructions means an abstraction has to be inserted in the
+    Rel(n) except for the initial terms given by user; in Pushed ((c,tm),deps,na),
+    [c] is the reference to the term (which is a Rel or an initial term), [tm] is
+    its type (telling whether we know if it is an inductive type or not),
+    [deps] is the list of terms to abstract before matching on [c] (these are
+    rels too)
+  - "Abstract" instructions mean that an abstraction has to be inserted in the
     current branch to build (this means a pattern has been detected dependent
-    in another one and generalisation is necessary to ensure well-typing)
-  - "Alias" instructions means an alias has to be inserted (this alias
+    in another one and a generalization is necessary to ensure well-typing)
+    Abstract instructions extend the [env] in which the other instructions
+    are typed
+  - "Alias" instructions mean an alias has to be inserted (this alias
     is usually removed at the end, except when its type is not the
     same as the type of the matched term from which it comes -
     typically because the inductive types are "real" parameters)
+  - "NonDepAlias" instructions mean the completion of a matching over
+    a term to match as for Alias but without inserting this alias
+    because there is no dependency in it
 
-  Right-hand-sides:
+  Right-hand sides:
 
   They consist of a raw term to type in an environment specific to the
   clause they belong to: the names of declarations are those of the
@@ -335,7 +289,7 @@ let inductive_template evdref env tmloc ind =
 	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1)
 	| Some b ->
-	    (b::subst,evarl,n+1))
+	    (substl subst b::subst,evarl,n+1))
       arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
@@ -347,13 +301,24 @@ let try_find_ind env sigma typ realnames =
       | None -> list_make (List.length realargs) Anonymous in
   IsInd (typ,ind,names)
 
-
 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
         un inductif cela doit être égal *)
   let _ = e_cumul env evdref expected_typ ty in ()
 
+let binding_vars_of_inductive = function
+  | NotInd _ -> []
+  | IsInd (_,IndType(_,realargs),_) -> List.filter isRel realargs
+
+let extract_inductive_data env sigma (_,b,t) =
+  if b<>None then (NotInd (None,t),[]) else
+  let tmtyp =
+    try try_find_ind env sigma t None
+    with Not_found -> NotInd (None,t) in
+  let tmtypvars = binding_vars_of_inductive tmtyp in
+  (tmtyp,tmtypvars)
+
 let unify_tomatch_with_patterns evdref env loc typ pats realnames =
   match find_row_ind pats with
     | None -> NotInd (None,typ)
@@ -370,7 +335,7 @@ let find_tomatch_tycon evdref env loc = function
       empty_tycon,None
 
 let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_rawconstr tomatch) in
+  let loc = Some (loc_of_glob_constr 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 !evdref j.uj_type in
@@ -466,6 +431,15 @@ let remove_current_pattern eqn =
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
     | [] -> anomaly "Empty list of patterns"
 
+let push_current_pattern (cur,ty) eqn =
+  match eqn.patterns with
+    | pat::pats ->
+        let rhs_env = push_rel (alias_of_pat pat,Some cur,ty) eqn.rhs.rhs_env in
+	{ eqn with
+            rhs = { eqn.rhs with rhs_env = rhs_env };
+	    patterns = pats }
+    | [] -> anomaly "Empty list of patterns"
+
 let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
 
 (**********************************************************************)
@@ -540,7 +514,7 @@ let is_dep_patt_in eqn = function
   | PatVar (_,name) -> occur_in_rhs name eqn.rhs
   | PatCstr _ -> true
 
-let mk_dep_patt_row (pats,eqn) =
+let mk_dep_patt_row (pats,_,eqn) =
   List.map (is_dep_patt_in eqn) pats
 
 let dependencies_in_pure_rhs nargs eqns =
@@ -554,8 +528,8 @@ let dependent_decl a = function
   | (na,Some c,t) -> dependent a t || dependent a c
 
 let rec dep_in_tomatch n = function
-  | (Pushed _ | Alias _) :: l -> dep_in_tomatch n l
-  | Abstract d :: l -> dependent_decl (mkRel n) d or dep_in_tomatch (n+1) l
+  | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch n l
+  | Abstract (_,d) :: l -> dependent_decl (mkRel n) d or dep_in_tomatch (n+1) l
   | [] -> false
 
 let dependencies_in_rhs nargs current tms eqns =
@@ -565,75 +539,90 @@ let dependencies_in_rhs nargs current tms eqns =
 
 (* Computing the matrix of dependencies *)
 
-(* We are in context d1...dn |- and [find_dependencies k 1 nextlist]
-   computes for declaration [k+1] in which of declarations in
-   [nextlist] (which corresponds to d(k+2)...dn) it depends;
-   declarations are expressed by index, e.g. in dependency list
-   [n-2;1], [1] points to [dn] and [n-2] to [d3] *)
+(* [find_dependency_list tmi [d(i+1);...;dn]] computes in which
+   declarations [d(i+1);...;dn] the term [tmi] is dependent in.
 
-let rec find_dependency_list k n = function
+   [find_dependencies_signature (used1,...,usedn) ((tm1,d1),...,(tmn,dn))]
+   returns [(deps1,...,depsn)] where [depsi] is a subset of n,..,i+1
+   denoting in which of the d(i+1)...dn, the term tmi is dependent.
+   Dependencies are expressed by index, e.g. in dependency list
+   [n-2;1], [1] points to [dn] and [n-2] to [d3]
+*)
+
+let rec find_dependency_list tmblock = function
   | [] -> []
   | (used,tdeps,d)::rest ->
-      let deps = find_dependency_list k (n+1) rest in
-      if used && dependent_decl (mkRel n) d
+      let deps = find_dependency_list tmblock rest in
+      if used && List.exists (fun x -> dependent_decl x d) tmblock
       then list_add_set (List.length rest + 1) (list_union deps tdeps)
       else deps
 
-let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) =
-  let deps = find_dependency_list k 1 nextlist in
+let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
+  let deps = find_dependency_list (tm::tmtypleaves) nextlist in
   if is_dep_or_cstr_in_rhs || deps <> []
-  then (k-1,(true ,deps,d)::nextlist)
-  else (k-1,(false,[]  ,d)::nextlist)
+  then ((true ,deps,d)::nextlist)
+  else ((false,[]  ,d)::nextlist)
 
 let find_dependencies_signature deps_in_rhs typs =
-  let k = List.length deps_in_rhs in
-  let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
+  let l = List.fold_right2 find_dependencies deps_in_rhs typs [] in
   List.map (fun (_,deps,_) -> deps) l
 
 (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
    and xn:Tn has just been regeneralized into x:Tn so that the terms
    to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
 
-   [regeneralize_index_tomatch n tomatch] updates t1..tq so that
-   former references to xn are now references to x. Note that t1..tq
-   are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
+   [relocate_index_tomatch n 1 tomatch] updates t1..tq so that
+   former references to xn1 are now references to x. Note that t1..tq
+   are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-.
+
+   [relocate_index_tomatch 1 n tomatch] will go the way back.
+ *)
 
-let regeneralize_index_tomatch n =
+let relocate_index_tomatch n1 n2 =
   let rec genrec depth = function
   | [] ->
       []
-  | Pushed ((c,tm),l,dep) :: rest ->
-      let c = regeneralize_index n depth c in
-      let tm = map_tomatch_type (regeneralize_index n depth) tm in
-      let l = List.map (regeneralize_rel n depth) l in
-      Pushed ((c,tm),l,dep) :: genrec depth rest
-  | Alias (c1,c2,d,t) :: rest ->
-      Alias (regeneralize_index n depth c1,c2,d,t) :: genrec depth rest
-  | Abstract d :: rest ->
-      Abstract (map_rel_declaration (regeneralize_index n depth) d)
+  | Pushed ((c,tm),l,na) :: rest ->
+      let c = relocate_index n1 n2 depth c in
+      let tm = map_tomatch_type (relocate_index n1 n2 depth) tm in
+      let l = List.map (relocate_rel n1 n2 depth) l in
+      Pushed ((c,tm),l,na) :: genrec depth rest
+  | Alias (na,c,d) :: rest ->
+      (* [c] is out of relocation scope *)
+      Alias (na,c,map_pair (relocate_index n1 n2 depth) d) :: genrec depth rest
+  | NonDepAlias :: rest ->
+      NonDepAlias :: genrec depth rest
+  | Abstract (i,d) :: rest ->
+      let i = relocate_rel n1 n2 depth i in
+      Abstract (i,map_rel_declaration (relocate_index n1 n2 depth) d)
       :: genrec (depth+1) rest in
   genrec 0
 
+(* [replace_tomatch n c tomatch] replaces [Rel n] by [c] in [tomatch] *)
+
 let rec replace_term n c k t =
-  if t = mkRel (n+k) then lift k c
+  if isRel t && destRel t = n+k then lift k c
   else map_constr_with_binders succ (replace_term n c) k t
 
-let length_of_tomatch_type_sign (dep,_) = function
-  | NotInd _ -> if dep<>Anonymous then 1 else 0
-  | IsInd (_,_,names) -> List.length names + if dep<>Anonymous then 1 else 0
+let length_of_tomatch_type_sign na = function
+  | NotInd _ -> if na<>Anonymous then 1 else 0
+  | IsInd (_,_,names) -> List.length names + if na<>Anonymous then 1 else 0
 
 let replace_tomatch n c =
   let rec replrec depth = function
   | [] -> []
-  | Pushed ((b,tm),l,dep) :: rest ->
+  | Pushed ((b,tm),l,na) :: rest ->
       let b = replace_term n c depth b in
       let tm = map_tomatch_type (replace_term n c depth) tm in
       List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l;
-      Pushed ((b,tm),l,dep) :: replrec depth rest
-  | Alias (c1,c2,d,t) :: rest ->
-      Alias (replace_term n c depth c1,c2,d,t) :: replrec depth rest
-  | Abstract d :: rest ->
-      Abstract (map_rel_declaration (replace_term n c depth) d)
+      Pushed ((b,tm),l,na) :: replrec depth rest
+  | Alias (na,b,d) :: rest ->
+      (* [b] is out of replacement scope *)
+      Alias (na,b,map_pair (replace_term n c depth) d) :: replrec depth rest
+  | NonDepAlias  :: rest ->
+      NonDepAlias :: replrec depth rest
+  | Abstract (i,d) :: rest ->
+      Abstract (i,map_rel_declaration (replace_term n c depth) d)
       :: replrec (depth+1) rest in
   replrec 0
 
@@ -646,16 +635,19 @@ let replace_tomatch n c =
 
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
-  | Pushed ((c,tm),l,dep)::rest ->
+  | Pushed ((c,tm),l,na)::rest ->
       let c = liftn n depth c in
       let tm = liftn_tomatch_type n depth tm in
       let l = List.map (fun i -> if i<depth then i else i+n) l in
-      Pushed ((c,tm),l,dep)::(liftn_tomatch_stack n depth rest)
-  | Alias (c1,c2,d,t)::rest ->
-      Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t)
+      Pushed ((c,tm),l,na)::(liftn_tomatch_stack n depth rest)
+  | Alias (na,c,d)::rest ->
+      Alias (na,liftn n depth c,map_pair (liftn n depth) d)
       ::(liftn_tomatch_stack n depth rest)
-  | Abstract d::rest ->
-      Abstract (map_rel_declaration (liftn n depth) d)
+  | NonDepAlias  :: rest ->
+      NonDepAlias :: liftn_tomatch_stack n depth rest
+  | Abstract (i,d)::rest ->
+      let i = if i<depth then i else i+n in
+      Abstract (i,map_rel_declaration (liftn n depth) d)
       ::(liftn_tomatch_stack n (depth+1) rest)
 
 let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -675,8 +667,14 @@ let lift_tomatch_stack n = liftn_tomatch_stack n 1
    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
-  interfere with user names *)
+   i.e. user names should be preserved and created names should not
+   interfere with user names
+
+   The exact names here are not important for typing (because they are
+   put in pb.env and not in the rhs.rhs_env of branches. However,
+   whether a name is Anonymous or not may have an effect on whether a
+   generalization is done or not.
+ *)
 
 let merge_name get_name obj = function
   | Anonymous -> get_name obj
@@ -687,15 +685,18 @@ 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,aliasname =
     List.fold_right
-      (fun (pats,eqn) names -> merge_names alias_of_pat pats names)
-      eqns names1 in
+      (fun (pats,pat_alias,eqn) (names,aliasname) ->
+        (merge_names alias_of_pat pats names,
+         merge_name (fun x -> x) pat_alias aliasname))
+      eqns (names1,Anonymous) in
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
-  let names4,_ =
+    List.fold_left (fun l (_,_,eqn) -> list_union l eqn.rhs.avoid_ids)
+      [] eqns in
+  let names3,_ =
     List.fold_left2
       (fun (l,avoid) d na ->
 	 let na =
@@ -705,10 +706,18 @@ let get_names env sign eqns =
 	 in
          (na::l,(out_name na)::avoid))
       ([],allvars) (List.rev sign) names2 in
-  names4
+  names3,aliasname
 
-(************************************************************************)
+(*****************************************************************)
 (* Recovering names for variables pushed to the rhs' environment *)
+(* We just factorized a match over a matrix of equations         *)
+(* "C xi1 .. xin as xi" as a single match over "C y1 .. yn as y" *)
+(* We now replace the names y1 .. yn y by the actual names       *)
+(* xi1 .. xin xi to be found in the i-th clause of the matrix    *)
+
+let set_declaration_name x (_,c,t) = (x,c,t)
+
+let recover_initial_subpattern_names = List.map2 set_declaration_name
 
 let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
 
@@ -716,68 +725,28 @@ let push_rels_eqn sign eqn =
   {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env} }
 
 let push_rels_eqn_with_names sign eqn =
-  let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
-  let sign = recover_alias_names alias_of_pat pats sign in
+  let subpats = List.rev (list_firstn (List.length sign) eqn.patterns) in
+  let subpatnames = List.map alias_of_pat subpats in
+  let sign = recover_initial_subpattern_names subpatnames sign in
   push_rels_eqn sign eqn
 
-let build_aliases_context env sigma names allpats pats =
-  (* pats is the list of bodies to push as an alias *)
-  (* They all are defined in env and we turn them into a sign *)
-  (* cuts in sign need to be done in allpats *)
-  let rec insert env sign1 sign2 n newallpats oldallpats = function
-    | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) ->
-        (* Anonymous leaves must be considered named and treated in the *)
-        (* next clause because they may occur in implicit arguments *)
-	insert env sign1 sign2
-	  n newallpats (List.map List.tl oldallpats) (pats,names)
-    | (deppat,nondeppat,d,t)::pats, na::names ->
-	let nondeppat = lift n nondeppat in
-	let deppat = lift n deppat in
-	let newallpats =
-	  List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
-	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)
-	  newallpats oldallpats (pats,names)
-    | [], [] -> newallpats, sign1, sign2, env
-    | _ -> anomaly "Inconsistent alias and name lists" in
-  let allpats = List.map (fun x -> [x]) allpats
-  in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names)
-
-let insert_aliases_eqn sign eqnnames alias_rest eqn =
-  let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
-  { eqn with
-      alias_stack = alias_rest;
-      rhs = {eqn.rhs with rhs_env = push_rels thissign eqn.rhs.rhs_env } }
-
-let insert_aliases env sigma alias eqns =
-  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
-  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
-  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
-  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 =
-    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 =
-    build_aliases_context env sigma [name2] eqnsnames [alias] in
-  let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in
-  sign2, env, eqns
+let push_generalized_decl_eqn env n (na,c,t) eqn =
+  let na = match na with
+  | Anonymous -> Anonymous
+  | Name id -> pi1 (Environ.lookup_rel n eqn.rhs.rhs_env) in
+  push_rels_eqn [(na,c,t)] eqn
 
-(**********************************************************************)
-(* Functions to deal with elimination predicate *)
+let drop_alias_eqn eqn =
+  { eqn with alias_stack = List.tl eqn.alias_stack }
 
-exception Occur
-let noccur_between_without_evar n m term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel p       -> if n<=p && p<n+m then raise Occur
-    | Evar (_,cl) -> ()
-    | _             -> iter_constr_with_binders succ occur_rec n c
-  in
-  (m = 0) or (try occur_rec n term; true with Occur -> false)
+let push_alias_eqn alias eqn =
+  let aliasname = List.hd eqn.alias_stack in
+  let eqn = drop_alias_eqn eqn in
+  let alias = set_declaration_name aliasname alias in
+  push_rels_eqn [alias] eqn
 
+(**********************************************************************)
+(* Functions to deal with elimination predicate *)
 
 (* Infering the predicate *)
 (*
@@ -797,8 +766,8 @@ Assume the types in the branches are the following
 
 Assume the type of the global case expression is Gamma |- T
 
-The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy
-the following n+1 equations:
+The predicate has the form phi = [y1..yq][z:I(y1..yq)]psi and it has to
+satisfy the following n+1 equations:
 
   Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1))  =  T1
    ...
@@ -808,11 +777,11 @@ the following n+1 equations:
 Some hints:
 
 - Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi)
-  => ..."  or a "psi(yk)", with psi extracting xij from uik, should be
+  => ... end"  or a "psi(yk)", with psi extracting xij from uik, should be
   inserted somewhere in Ti.
 
-- If T is undefined, an easy solution is to insert a "match z with (Ci
-  xi1..xipi) => ..." in front of each Ti
+- If T is undefined, an easy solution is to insert a "match z with
+  (Ci xi1..xipi) => ... end" in front of each Ti
 
 - Otherwise, T1..Tn and T must be step by step unified, if some of them
   diverge, then try to replace the diverging subterm by one of y1..yq or z.
@@ -825,10 +794,10 @@ Some hints:
 
 let rec map_predicate f k ccl = function
   | [] -> f k ccl
-  | Pushed ((_,tm),_,dep) :: rest ->
-      let k' = length_of_tomatch_type_sign dep tm in
+  | Pushed ((_,tm),_,na) :: rest ->
+      let k' = length_of_tomatch_type_sign na tm in
       map_predicate f (k+k') ccl rest
-  | Alias _ :: rest ->
+  | (Alias _ | NonDepAlias) :: rest ->
       map_predicate f k ccl rest
   | Abstract _ :: rest ->
       map_predicate f (k+1) ccl rest
@@ -839,7 +808,7 @@ let liftn_predicate n = map_predicate (liftn n)
 
 let lift_predicate n = liftn_predicate n 1
 
-let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0
+let regeneralize_index_predicate n = map_predicate (relocate_index n 1) 0
 
 let substnl_predicate sigma = map_predicate (substnl sigma)
 
@@ -867,55 +836,74 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
 (* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x'        *)
 (* then we have to replace x by x' in t(x) and y by y' in P                  *)
 (*****************************************************************************)
-let generalize_predicate (names,(nadep,_)) ny d tms ccl =
-  if nadep=Anonymous then anomaly "Undetected dependency";
+let generalize_predicate (names,na) ny d tms ccl =
+  if na=Anonymous then anomaly "Undetected dependency";
   let p = List.length names + 1 in
   let ccl = lift_predicate 1 ccl tms in
   regeneralize_index_predicate (ny+p+1) ccl tms
 
+(*****************************************************************************)
+(* We just matched over cur:ind(realargs) in the following matching problem  *)
+(*                                                                           *)
+(*   env |- match cur tms return ccl with ... end                            *)
+(*                                                                           *)
+(* and we want to build the predicate corresponding to the individual        *)
+(* matching over cur                                                         *)
+(*                                                                           *)
+(*    pred = fun X:realargstyps x:ind(X)] PI tms.ccl                         *)
+(*                                                                           *)
+(* where pred is computed by abstract_predicate and PI tms.ccl by            *)
+(* extract_predicate                                                         *)
+(*****************************************************************************)
 let rec extract_predicate ccl = function
-   | Alias (deppat,nondeppat,_,_)::tms ->
-       (* substitution already done in build_branch *)
+  | (Alias _ | NonDepAlias)::tms ->
+      (* substitution already done in build_branch *)
       extract_predicate ccl tms
-  | Abstract d::tms ->
-      mkProd_or_LetIn d (extract_predicate ccl tms)
-  | Pushed ((cur,NotInd _),_,(dep,_))::tms ->
-      let tms = if dep<>Anonymous then lift_tomatch_stack 1 tms else tms in
+  | Abstract (i,d)::tms ->
+      mkProd_wo_LetIn d (extract_predicate ccl tms)
+  | Pushed ((cur,NotInd _),_,na)::tms ->
+      let tms = if na<>Anonymous then lift_tomatch_stack 1 tms else tms in
       let pred = extract_predicate ccl tms in
-      if dep<>Anonymous then subst1 cur pred else pred
-  | Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,(dep,_))::tms ->
+      if na<>Anonymous then subst1 cur pred else pred
+  | Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,na)::tms ->
       let realargs = List.rev realargs in
-      let k = if dep<>Anonymous then 1 else 0 in
+      let k = if na<>Anonymous then 1 else 0 in
       let tms = lift_tomatch_stack (List.length realargs + k) tms in
       let pred = extract_predicate ccl tms in
-      substl (if dep<>Anonymous then cur::realargs else realargs) pred
+      substl (if na<>Anonymous then cur::realargs else realargs) pred
   | [] ->
       ccl
 
-let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
+let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let sign = make_arity_signature env true indf in
-  (* n is the number of real args + 1 *)
+  (* n is the number of real args + 1 (+ possible let-ins in sign) *)
   let n = List.length sign in
-  let tms = lift_tomatch_stack n tms in
-  let tms =
-    match kind_of_term cur with
-      | 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
+  (* Before abstracting we generalize over cur and on those realargs *)
+  (* that are rels, consistently with the specialization made in     *)
+  (* build_branch                                                    *)
+  let tms = List.fold_right2 (fun par arg tomatch ->
+    match kind_of_term par with
+    | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch
+    | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign)
+       (lift_tomatch_stack n tms) in
+  (* Pred is already dependent in the current term to match (if      *)
+  (* (na<>Anonymous) and its realargs; we just need to adjust it to  *)
+  (* full sign if dep in cur is not taken into account               *)
+  let ccl = if na <> Anonymous then ccl else lift_predicate 1 ccl tms in
   let pred = extract_predicate ccl tms in
+  (* Build the predicate properly speaking *)
+  let sign = List.map2 set_declaration_name (na::names) sign in
   it_mkLambda_or_LetIn_name env pred sign
 
-let known_dependent (_,dep) = (dep = KnownDep)
-
 (* [expand_arg] is used by [specialize_predicate]
-   it replaces gamma, x1...xn, x1...xk |- pred
-   by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or
-   by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *)
+   if Yk denotes [Xk;xk] or [Xk],
+   it replaces gamma, x1...xn, x1...xk Yk+1...Yn |- pred
+   by gamma, x1...xn, x1...xk-1 [Xk;xk] Yk+1...Yn |- pred (if dep) or
+   by gamma, x1...xn, x1...xk-1 [Xk] Yk+1...Yn |- pred (if not dep) *)
 
-let expand_arg tms ccl ((_,t),_,na) =
+let expand_arg tms (p,ccl) ((_,t),_,na) =
   let k = length_of_tomatch_type_sign na t in
-  lift_predicate (k-1) ccl tms
+  (p+k,liftn_predicate (k-1) (p+1) ccl tms)
 
 let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
@@ -926,7 +914,7 @@ let adjust_impossible_cases pb pred tomatch submat =
       (* 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
+	map_succeed (function Alias _ | NonDepAlias -> Anonymous | _ -> failwith"") tomatch
       in
       [ { patterns = pats;
           rhs = { rhs_env = pb.env;
@@ -942,71 +930,132 @@ let adjust_impossible_cases pb pred tomatch submat =
     submat
 
 (*****************************************************************************)
-(* pred = [X:=realargs;x:=c]P types the following problem:                   *)
+(* Let  pred = PI [X;x:I(X)]. PI tms. P  be a typing predicate for the       *)
+(* following pattern-matching problem:                                       *)
 (*                                                                           *)
-(*  Gamma |- match Pushed(c:I(realargs)) rest with...end: pred               *)
+(*  Gamma |- match Pushed(c:I(V)) as x in I(X), tms return pred with...end   *)
 (*                                                                           *)
 (* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi)      *)
-(* is considered. Assume each Ti is some Ii(argsi).                          *)
-(* We let e=Ci(x1,...,xn) and replace pred by                                *)
+(* is considered. Assume each Ti is some Ii(argsi) with Ti:PI Ui. sort_i     *)
+(* We let subst = X:=realargsi;x:=Ci(x1,...,xn) and replace pred by          *)
 (*                                                                           *)
-(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *)
+(* pred' = PI [X1:Ui;x1:I1(X1)]...[Xn:Un;xn:In(Xn)]. (PI tms. P)[subst]      *)
 (*                                                                           *)
-(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
+(* s.t. the following well-typed sub-pattern-matching problem is obtained    *)
+(*                                                                           *)
+(* Gamma,x'1..x'n |-                                                         *)
+(*   match                                                                   *)
+(*      Pushed(x'1) as x1 in I(X1),                                          *)
+(*      ..,                                                                  *)
+(*      Pushed(x'n) as xn in I(Xn),                                          *)
+(*      tms                                                                  *)
+(*      return pred'                                                         *)
+(*   with .. end                                                             *)
 (*                                                                           *)
 (*****************************************************************************)
-let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
-  (* Assume some gamma st: gamma, (X,x:=realargs,copt), tms |- ccl *)
+let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
+  (* Assume some gamma st: gamma |- PI [X,x:I(X)]. PI 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' *)
+  (* We adjust pred st: gamma, x1..xn |- PI [X,x:I(X)]. PI tms. ccl' *)
+  (* so that x can later be instantiated by Ci(x1..xn) *)
+  (* and X by the realargs for Ci *)
   let n = cs.cs_nargs in
   let ccl' = liftn_predicate n (k+1) ccl tms in
-  let argsi =
+  (* We prepare the substitution of X and x:I(X) *)
+  let realargsi =
     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'' *)
+  let copti =
+    if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
+  (* The substituends realargsi, copti are all defined in gamma, x1...xn *)
+  (* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *)
+  (* Note: applying the substitution in tms is not important (is it sure?) *)
   let ccl'' =
-    whd_betaiota Evd.empty (subst_predicate (argsi, copti) ccl' tms) in
-  (* We adjust ccl st: gamma, x1..xn, x1..xn, tms |- ccl'' *)
+    whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
+  (* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
-  (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
-  List.fold_left (expand_arg tms) ccl''' newtomatchs
+  (* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
+  snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env !evdref indf current dep tms p in
+  let pred = abstract_predicate env !evdref indf current realargs dep tms p in
   (pred, whd_betaiota !evdref
-           (applist (pred, realargs@[current])), new_Type ())
+           (applist (pred, realargs@[current])))
 
 (* Take into account that a type has been discovered to be inductive, leading
    to more dependencies in the predicate if the type has indices *)
 let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb =
-  let ((_,oldtyp),deps,((nadep,_) as dep)) = tomatch in
+  let ((_,oldtyp),deps,na) = tomatch in
   match typ, oldtyp with
   | IsInd (_,_,names), NotInd _ ->
-      let k = if nadep <> Anonymous then 2 else 1 in
+      let k = if na <> Anonymous then 2 else 1 in
       let n = List.length names in
       { pb with pred = liftn_predicate n k pb.pred pb.tomatch },
-      (ct,List.map (fun i -> if i >= k then i+n else i) deps,dep)
+      (ct,List.map (fun i -> if i >= k then i+n else i) deps,na)
   | _ ->
-      pb, (ct,deps,dep)
+      pb, (ct,deps,na)
+
+(* Remove commutative cuts that turn out to be non-dependent after
+   some evars have been instantiated *)
+
+let rec ungeneralize n ng body =
+  match kind_of_term body with
+  | Lambda (_,_,c) when ng = 0 ->
+      subst1 (mkRel n) c
+  | Lambda (na,t,c) ->
+      (* We traverse an inner generalization *)
+      mkLambda (na,t,ungeneralize (n+1) (ng-1) c)
+  | LetIn (na,b,t,c) ->
+      (* We traverse an alias *)
+      mkLetIn (na,b,t,ungeneralize (n+1) ng c)
+  | Case (ci,p,c,brs) ->
+      (* We traverse a split *)
+      let p =
+        let sign,p = decompose_lam_assum p in
+        let sign2,p = decompose_prod_n_assum ng p in
+        let p = prod_applist p [mkRel (n+List.length sign+ng)] in
+        it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
+      mkCase (ci,p,c,array_map2 (fun q c ->
+        let sign,b = decompose_lam_n_assum q c in
+        it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
+        ci.ci_cstr_ndecls brs)
+  | App (f,args) ->
+      (* We traverse an inner generalization *)
+      assert (isCase f);
+      mkApp (ungeneralize n (ng+Array.length args) f,args)
+  | _ -> assert false
+
+let ungeneralize_branch n k (sign,body) cs =
+  (sign,ungeneralize (n+cs.cs_nargs) k body)
+
+let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
+  let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
+  | [], _ -> brs,tomatch,pred,[]
+  | n::deps, Abstract (i,d) :: tomatch ->
+      let d = map_rel_declaration (nf_evar evd) d in
+      if List.exists (fun c -> dependent_decl (lift k c) d) tocheck || pi2 d <> None then
+        (* Dependency in the current term to match and its dependencies is real *)
+        let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in
+        let inst = if pi2 d = None then mkRel n::inst else inst in
+        brs, Abstract (i,d) :: tomatch, pred, inst
+      else
+        (* Finally, no dependency remains, so, we can replace the generalized *)
+        (* terms by its actual value in both the remaining terms to match and *)
+        (* the bodies of the Case *)
+        let pred = lift_predicate (-1) pred tomatch in
+        let tomatch = relocate_index_tomatch 1 (n+1) tomatch in
+        let tomatch = lift_tomatch_stack (-1) tomatch in
+        let brs = array_map2 (ungeneralize_branch n k) brs cs in
+        aux k brs tomatch pred tocheck deps
+  | _ -> assert false
+  in aux 0 brs tomatch pred tocheck deps
 
 (************************************************************************)
 (* Sorting equations by constructor *)
 
-type inversion_problem =
-  (* the discriminating arg in some Ind and its order in Ind *)
-  | Incompatible of int * (int * int)
-  | Constraints of (int * constr) list
-
-let solve_constraints constr_info indt =
-  (* TODO *)
-  Constraints []
-
 let rec irrefutable env = function
   | PatVar (_,name) -> true
   | PatCstr (_,cstr,args,_) ->
@@ -1034,12 +1083,12 @@ let group_equations pb ind current cstrs mat =
 	       (* 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
-		 brs.(i-1) <- (args, rest) :: brs.(i-1)
+		 brs.(i-1) <- (args, name, rest) :: brs.(i-1)
 	       done
-	   | PatCstr (loc,((_,i)),args,_) ->
+	   | PatCstr (loc,((_,i)),args,name) ->
 	       (* This is a regular clause *)
 	       only_default := false;
-	       brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
+	       brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in
   (brs,!only_default)
 
 (************************************************************************)
@@ -1047,16 +1096,18 @@ let group_equations pb ind current cstrs mat =
 
 (* Abstracting over dependent subterms to match *)
 let rec generalize_problem names pb = function
-  | [] -> pb
+  | [] -> pb, []
   | i::l ->
-      let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+      let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+      let pb',deps = generalize_problem names pb l in
+      if na = Anonymous & b <> None then pb',deps else
       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
+      let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
       { pb' with
-	  tomatch = Abstract d :: tomatch;
-          pred = generalize_predicate names i d pb.tomatch pb'.pred  }
+	  tomatch = Abstract (i,d) :: tomatch;
+          pred = generalize_predicate names i d pb'.tomatch pb'.pred  },
+      i::deps
 
 (* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
@@ -1064,87 +1115,92 @@ let build_leaf pb =
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
   j_nf_evar !(pb.evdref) j
 
-(* Building the sub-problem when all patterns are variables *)
-let shift_problem ((current,t),_,(nadep,_)) pb =
-  {pb with
-     tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = specialize_predicate_var (current,t,nadep) pb.tomatch pb.pred;
-     history = push_history_pattern 0 AliasLeaf pb.history;
-     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 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
-      DepAlias
-  in
+(* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
+let build_branch current realargs deps (realnames,curname) pb arsign eqns const_info =
+  (* We remember that we descend through constructor C *)
   let history =
-    push_history_pattern const_info.cs_nargs
-      (AliasConstructor const_info.cs_cstr)
-      pb.history in
+    push_history_pattern const_info.cs_nargs const_info.cs_cstr pb.history in
 
-  (* We find matching clauses *)
+  (* We prepare the matching on x1:T1 .. xn:Tn using some heuristic to *)
+  (* build the name x1..xn from the names present in the equations *)
+  (* that had matched constructor C *)
   let cs_args = const_info.cs_args in
-  let names = get_names pb.env cs_args eqns in
-  let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
+  let names,aliasname = get_names pb.env cs_args eqns in
   let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in
 
+  (* We build the matrix obtained by expanding the matching on *)
+  (* "C x1..xn as x" followed by a residual matching on eqn into *)
+  (* a matching on "x1 .. xn eqn" *)
+  let submat = List.map (fun (tms,_,eqn) -> prepend_pattern tms eqn) eqns in
+
+  (* We adjust the terms to match in the context they will be once the *)
+  (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
+  let typs' =
+    list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
+
+  let extenv = push_rels typs pb.env in
+
+  let typs' =
+    List.map (fun (c,d) ->
+      (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in
+
+  (* We compute over which of x(i+1)..xn and x matching on xi will need a *)
+  (* generalization *)
   let dep_sign =
     find_dependencies_signature
       (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns)
-      (List.rev typs) in
+      (List.rev typs') in
 
   (* 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
 
-  (* We replace [(mkRel 1)] by its expansion [ci] *)
-  (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *)
-  (* This is done in two steps : first from "Gamma |- tms" *)
-  (* into  "Gamma; typs; curalias |- tms" *)
-  let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
+  (* Current context Gamma has the form Gamma1;cur:I(realargs);Gamma2 *)
+  (* We go from Gamma |- PI tms. pred to                              *)
+  (* Gamma;x1..xn;curalias:I(x1..xn) |- PI tms'. pred'                *)
+  (* where, in tms and pred, those realargs that are vars are         *)
+  (* replaced by the corresponding xi and cur replaced by curalias    *)
+  let cirealargs = Array.to_list const_info.cs_concl_realargs in
 
-  let tomatch = match kind_of_term current with
-    | Rel i -> replace_tomatch (i+const_info.cs_nargs) ci tomatch
-    | _ -> (* non-rel initial term *) tomatch in
+  (* Do the specialization for terms to match *)
+  let tomatch = List.fold_right2 (fun par arg tomatch ->
+    match kind_of_term par with
+    | Rel i -> replace_tomatch (i+const_info.cs_nargs) arg tomatch
+    | _ -> tomatch) (current::realargs) (ci::cirealargs)
+      (lift_tomatch_stack const_info.cs_nargs pb.tomatch) in
 
   let pred_is_not_dep =
     noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
 
   let typs' =
-    list_map2_i
-      (fun i d deps ->
-        let (na,c,t) = map_rel_declaration (lift i) d in
-	let dep = match dep with
-	  | Name _ as na',k -> (if na <> Anonymous then na else na'),k
-	  | Anonymous,KnownNotDep ->
-	      if deps = [] && pred_is_not_dep then
-		(Anonymous,KnownNotDep)
-	      else
-		(force_name na,KnownDep)
-	  | _,_ -> anomaly "Inconsistent dependency" in
-	((mkRel i, NotInd (c,t)),deps,dep))
-      1 typs (List.rev dep_sign) in
-
+    List.map2
+      (fun (tm,(tmtyp,_),(na,_,_)) deps ->
+	let na = match curname with
+	| Name _ -> (if na <> Anonymous then na else curname)
+	| Anonymous ->
+	    if deps = [] && pred_is_not_dep then Anonymous else force_name na in
+	((tm,tmtyp),deps,na))
+      typs' (List.rev dep_sign) in
+
+  (* Do the specialization for the predicate *)
   let pred =
-    specialize_predicate typs' (realnames,dep) arsign const_info tomatch pb.pred in
+    specialize_predicate typs' (realnames,curname) arsign const_info tomatch pb.pred in
 
   let currents = List.map (fun x -> Pushed x) typs' in
 
-  let ind =
-    appvect (
-      applist (mkInd (inductive_of_constructor const_info.cs_cstr),
-      List.map (lift const_info.cs_nargs) const_info.cs_params),
-      const_info.cs_concl_realargs) in
+  let alias =
+    if aliasname = Anonymous then
+      NonDepAlias
+    else
+      let cur_alias = lift const_info.cs_nargs current in
+      let ind =
+        appvect (
+          applist (mkInd (inductive_of_constructor const_info.cs_cstr),
+                   List.map (lift const_info.cs_nargs) const_info.cs_params),
+          const_info.cs_concl_realargs) in
+      Alias (aliasname,cur_alias,(ci,ind)) in
 
-  let cur_alias = lift (List.length typs) current in
-  let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
-  let tomatch = List.rev_append currents tomatch in
+  let tomatch = List.rev_append (alias :: currents) tomatch in
 
   let submat = adjust_impossible_cases pb pred tomatch submat in
   if submat = [] then
@@ -1153,7 +1209,7 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
 
   typs,
   { pb with
-      env = push_rels typs pb.env;
+      env = extenv;
       tomatch = tomatch;
       pred = pred;
       history = history;
@@ -1162,11 +1218,11 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
 (**********************************************************************
  INVARIANT:
 
-  pb = { env, subst, tomatch, mat, ...}
-  tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T)
+  pb = { env, pred, tomatch, mat, ...}
+  tomatch = list of Pushed (c:T), Abstract (na:T), Alias (c:T) or NonDepAlias
 
-  "Pushed" terms and types are relative to env
-  "Abstract" types are relative to env enriched by the previous terms to match
+  all terms and types in Pushed, Abstract and Alias are relative to env
+  enriched by the Abstract coming before
 
 *)
 
@@ -1174,9 +1230,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
 (* Main compiling descent *)
 let rec compile pb =
   match pb.tomatch with
-    | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur
-    | (Alias x)::rest -> compile_alias pb x rest
-    | (Abstract d)::rest -> compile_generalization pb d rest
+    | Pushed cur :: rest -> match_current { pb with tomatch = rest } cur
+    | Alias x :: rest -> compile_alias pb x rest
+    | NonDepAlias :: rest -> compile_non_dep_alias pb rest
+    | Abstract (i,d) :: rest -> compile_generalization pb i d rest
     | [] -> build_leaf pb
 
 (* Case splitting *)
@@ -1187,63 +1244,108 @@ and match_current pb tomatch =
   match typ with
     | NotInd (_,typ) ->
 	check_all_variables typ pb.mat;
-	compile (shift_problem tomatch pb)
+	shift_problem tomatch pb
     | 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 tomatch pb)
+	  shift_problem tomatch pb
 	else
-          let _constraints = Array.map (solve_constraints indt) cstrs in
-
 	  (* We generalize over terms depending on current term to match *)
-	  let pb = generalize_problem (names,dep) pb deps in
+	  let pb,deps = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brs = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in
-
+	  let brvals = array_map2 (compile_branch current realargs (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) =
+          let depstocheck = current::binding_vars_of_inductive typ in
+          let brvals,tomatch,pred,inst =
+            postprocess_dependencies !(pb.evdref) depstocheck
+              brvals pb.tomatch pb.pred deps cstrs in
+          let brvals = Array.map (fun (sign,body) ->
+            it_mkLambda_or_LetIn body sign) brvals in
+	  let (pred,typ) =
 	    find_predicate pb.caseloc pb.env pb.evdref
-	      pb.pred current indt (names,dep) pb.tomatch in
+	      pred current indt (names,dep) 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
-	  let inst = List.map mkRel deps in
+	  let pred = nf_betaiota !(pb.evdref) pred in
+	  let case = mkCase (ci,pred,current,brvals) in
+	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
 
-and compile_branch current names deps pb arsign eqn cstr =
-  let sign, pb = build_branch current deps names pb arsign eqn cstr in
+(* Building the sub-problem when all patterns are variables *)
+and shift_problem ((current,t),_,na) pb =
+  let ty = type_of_tomatch t in
+  let tomatch = lift_tomatch_stack 1 pb.tomatch in
+  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pb =
+    { pb with
+       env = push_rel (na,Some current,ty) pb.env;
+       tomatch = tomatch;
+       pred = lift_predicate 1 pred tomatch;
+       history = pop_history pb.history;
+       mat = List.map (push_current_pattern (current,ty)) pb.mat } in
   let j = compile pb in
-  (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
+  { uj_val = subst1 current j.uj_val;
+    uj_type = subst1 current j.uj_type }
 
-and compile_generalization pb d rest =
+(* Building the sub-problem when all patterns are variables *)
+and compile_branch current realargs names deps pb arsign eqns cstr =
+  let sign, pb = build_branch current realargs deps names pb arsign eqns cstr in
+  sign, (compile pb).uj_val
+
+(* Abstract over a declaration before continuing splitting *)
+and compile_generalization pb i d rest =
   let pb =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       mat = List.map (push_rels_eqn [d]) pb.mat } in
+       mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in
   let j = compile pb in
   { uj_val = mkLambda_or_LetIn d j.uj_val;
-    uj_type = mkProd_or_LetIn d j.uj_type }
+    uj_type = mkProd_wo_LetIn d j.uj_type }
 
-and compile_alias pb aliases rest =
-  let history = simplify_history pb.history in
-  let sign, newenv, mat = insert_aliases pb.env !(pb.evdref) aliases pb.mat in
-  let n = List.length sign in
-  let tomatch = lift_tomatch_stack n rest in
+and compile_alias pb (na,orig,(expanded,expanded_typ)) rest =
+  let f c t =
+    let alias = (na,Some c,t) in
+    let pb =
+      { pb with
+         env = push_rel alias pb.env;
+         tomatch = lift_tomatch_stack 1 rest;
+         pred = lift_predicate 1 pb.pred pb.tomatch;
+         history = pop_history_pattern pb.history;
+         mat = List.map (push_alias_eqn alias) pb.mat } in
+    let j = compile pb in
+    { uj_val =
+        if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then
+          subst1 c j.uj_val
+        else
+          mkLetIn (na,c,t,j.uj_val);
+      uj_type = subst1 c j.uj_type } in
+  if isRel orig or isVar orig then
+    (* Try to compile first using non expanded alias *)
+    try f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+    with e when precatchable_exception e ->
+    (* Try then to compile using expanded alias *)
+    f expanded expanded_typ
+  else
+    (* Try to compile first using expanded alias *)
+    try f expanded expanded_typ
+    with e when precatchable_exception e ->
+    (* Try then to compile using non expanded alias *)
+    f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+
+
+(* Remember that a non-trivial pattern has been consumed *)
+and compile_non_dep_alias pb rest =
   let pb =
-    {pb with
-       env = newenv;
-       tomatch = tomatch;
-       pred = lift_predicate n pb.pred tomatch;
-       history = history;
-       mat = mat } in
-  let j = compile pb in
-  List.fold_left mkSpecialLetInJudge j sign
+    { pb with
+       tomatch = rest;
+       history = pop_history_pattern pb.history;
+       mat = List.map drop_alias_eqn pb.mat } in
+  compile pb
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
 substituer après par les initiaux *)
@@ -1260,7 +1362,7 @@ let matx_of_eqns env tomatchl eqns =
     let initial_rhs = rhs in
     let rhs =
       { rhs_env = env;
-        rhs_vars = free_rawvars initial_rhs;
+        rhs_vars = free_glob_vars initial_rhs;
 	avoid_ids = ids@(ids_of_named_context (named_context env));
 	it = Some initial_rhs } in
     { patterns = initial_lpat;
@@ -1273,7 +1375,7 @@ let matx_of_eqns env tomatchl eqns =
 (***************** Building an inversion predicate ************************)
 
 (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T"
-   be a pattern-matching problem. We assume that the each uij can be
+   be a pattern-matching problem. We assume that each uij can be
    decomposed under the form pij(vij1..vijq_ij) where pij(aij1..aijq_ij)
    is a pattern depending on some variables aijk and the vijk are
    instances of these variables.  We also assume that each ti has the
@@ -1314,26 +1416,23 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
     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 extenv)
-      | None ->
-	  (n,ty) 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
-      (p,u,(expand_vars_in_term extenv u,lift p ty))
-    else
-      failwith "") subst in
+    let rec traverse_local_defs p =
+      match pi2 (lookup_rel p extenv) with
+      | Some c -> assert (isRel c); traverse_local_defs (p + destRel c)
+      | None -> p in
+    let p = traverse_local_defs p in
+    let u = lift (n'-n) u in
+    (p,u,expand_vars_in_term extenv u)) subst in
   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 rec list_assoc_in_triple x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
+
 (* 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.
@@ -1359,46 +1458,62 @@ 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 t = whd_evar !evdref t in match kind_of_term t with
+    | Rel n when pi2 (lookup_rel n env) <> None ->
+        map_constr_with_full_binders push_binder aux x t
+    | Evar ev ->
+        let ty = get_type_of env sigma t in
+        let inst =
+	  list_map_i
+	    (fun i _ ->
+              try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
+              1 (rel_context env) in
+        let ev = e_new_evar evdref env ~src:(loc, CasesType) ty in
+        evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
+        ev
+    | _ ->
     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 u = pi3 (List.hd good) in (* u is in extenv *)
       let vl = List.map pi1 good in
+      let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
+      let depvl = free_rels ty in
       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 =
-	List.map (fun a -> not (isRel a) or dependent a u) inst in
+	List.map (fun a -> not (isRel a) || dependent a u
+                           || Intset.mem (destRel a) depvl) inst in
       let named_filter =
 	List.map (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
       let filter = rel_filter@named_filter in
+      let candidates = u :: List.map mkRel vl in
       let ev =
-	e_new_evar evdref extenv ~src:(loc, CasesType) ~filter:filter ty in
-      evdref := add_conv_pb (Reduction.CONV,extenv,substl inst ev,u) !evdref;
+	e_new_evar evdref extenv ~src:(loc, CasesType) ~filter ~candidates ty in
       lift k ev
     else
       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
+  let t,tt = match t with
     | None ->
 	(* 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 tt = new_Type () in
 	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
-  try get_judgment_of extenv !evdref t
-  with Not_found | Anomaly _ ->
-    (* Quick workaround to acknowledge failure to build a well-typed pred *)
-    error "Unable to infer a well-typed return clause."
+	  e_new_evar evdref env ~src:(loc,ImpossibleCase) tt in
+	(lift (n'-n) impossible_case_type, tt)
+    | Some t ->
+        let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
+        let evd,tt = Typing.e_type_of extenv !evdref t in
+        evdref := evd;
+        (t,tt) in
+  { uj_val = t; uj_type = tt }
 
 (* 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
@@ -1432,12 +1547,16 @@ let build_inversion_problem loc env sigma tms t =
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
+	let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
 	let p = List.length realargs in
 	let env' = push_rels sign env in
 	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
 	patl@pat::patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
-	aux n env acc_sign tms acc in
+      let pat,acc = make_patvar t acc in
+      let d = (alias_of_pat pat,None,t) in
+      let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
+      pat::patl,acc_sign,acc in
   let avoid0 = ids_of_context env in
   (* [patl] is a list of patterns revealing the substructure of
      constructors present in the constraints on the type of the
@@ -1450,16 +1569,22 @@ let build_inversion_problem loc env sigma tms t =
      problem have to be abstracted *)
   let patl,sign,(subst,avoid) = aux 0 env [] tms ([],avoid0) in
   let n = List.length sign in
-  let (pb_env,_),sub_tms =
-    list_fold_map (fun (env,i) (na,b,t as d) ->
-      let typ =
-	if b<>None then NotInd(None,t) else
-	  try try_find_ind env sigma t None
-	  with Not_found -> NotInd (None,t) in
-      let ty = lift_tomatch_type (n-i) typ in
-      let tm = Pushed ((mkRel (n-i),ty),[],(Anonymous,KnownNotDep)) in
-      ((push_rel d env,i+1),tm))
-      (env,0) (List.rev sign) in
+
+  let decls =
+    list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+
+  let pb_env = push_rels sign env in
+  let decls =
+    List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
+
+  let decls = List.rev decls in
+  let dep_sign = find_dependencies_signature (list_make n true) decls in
+
+  let sub_tms =
+    List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
+      let na = if deps = [] then Anonymous else force_name na in
+      Pushed ((tm,tmtyp),deps,na))
+      dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
   (* [eqn1] is the first clause of the auxiliary pattern-matching that
      serves as skeleton for the return type: [patl] is the
@@ -1508,26 +1633,14 @@ let build_inversion_problem loc env sigma tms t =
 
 (* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
-let build_initial_predicate knowndep allnames pred =
-  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
-  let rec buildrec n pred nal = function
-    | [] -> List.rev nal,pred
-    | names::lnames ->
-        let names' = List.tl names in
-        let n' = n + List.length names' in
-        let pred, p =
-          if dependent (mkRel (nar-n')) pred then pred, 1
-          else liftn (-1) (nar-n') pred, 0 in
-        let na =
-          if p=1 then
-            let na = List.hd names in
-            ((if na = Anonymous then
-              (* can happen if evars occur in the return clause *)
-              Name (id_of_string "x") (*Hum*)
-            else na),knowndep)
-          else (Anonymous,KnownNotDep) in
-        buildrec (n'+1) pred (na::nal) lnames
-  in buildrec 0 pred [] allnames
+let build_initial_predicate arsign pred =
+  let rec buildrec n pred tmnames = function
+    | [] -> List.rev tmnames,pred
+    | ((na,c,t)::realdecls)::lnames ->
+        let n' = n + List.length realdecls in
+        buildrec (n'+1) pred (force_name na::tmnames) lnames
+    | _ -> assert false
+  in buildrec 0 pred [] (List.rev arsign)
 
 let extract_arity_signature env0 tomatchl tmsign =
   let get_one_sign n tm (na,t) =
@@ -1553,19 +1666,11 @@ let extract_arity_signature env0 tomatchl tmsign =
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_make nrealargs_ctxt Anonymous in
-(* 	  let na =  *)
-(* 	    match na with  *)
-(* 	      | Name _ -> na *)
-(* 	      | Anonymous -> *)
-(* 		  match kind_of_term term with *)
-(* 		    | Rel n -> pi1 (lookup_rel n (Environ.rel_context env0)) *)
-(* 		    | _ -> Anonymous *)
-(* 	  in *)
 	  (na,None,build_dependent_inductive env0 indf')
 	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
   let rec buildrec n = function
     | [],[] -> []
-    | (_,tm)::ltm, x::tmsign ->
+    | (_,tm)::ltm, (_,x)::tmsign ->
 	let l = get_one_sign n tm x in
 	l :: buildrec (n + List.length l) (ltm,tmsign)
     | _ -> assert false
@@ -1581,7 +1686,7 @@ 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 tomatchs sign arsign c =
+let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len =
     List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
@@ -1635,9 +1740,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
-  let arsign = extract_arity_signature env tomatchs sign in
-  let names = List.rev (List.map (List.map pi1) arsign) in
+let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No type annotation *)
@@ -1646,40 +1749,40 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
         (* 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
+          prepare_predicate_from_arsign_tycon loc tomatchs 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) ->
-	(* First strategy: we build an "inversion" predicate *)
-	let sigma1,pred = build_inversion_problem loc env !evdref tomatchs t in
-	(* Second strategy: we abstract the tycon wrt to the dependencies *)
-        let pred2 = lift (List.length names) t in
-	[sigma1, DepUnknown, pred; !evdref, KnownNotDep, pred2]
-    | 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
+	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
+	[sigma, pred1; sigma2, pred2]
+    | None, _ ->
+	(* No dependent type constraint, or no constraints at all: *)
+	(* we use two strategies *)
+        let sigma,t = match tycon with
+	| Some (None, t) -> sigma,t
+	| _ -> new_type_evar sigma env ~src:(loc, CasesType) in
+        (* First strategy: we build an "inversion" predicate *)
+	let sigma1,pred1 = build_inversion_problem loc env sigma 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]
+        let pred2 = lift (List.length arsign) t in
+	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
-      let env = List.fold_right push_rels arsign env in
-      let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in
-      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]
+      let envar = List.fold_right push_rels arsign env in
+      let sigma, newt = new_sort_variable sigma in
+      let evdref = ref sigma in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
+      let sigma = Option.cata (fun tycon ->
+          let na = Name (id_of_string "x") in
+          let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in
+          let predinst = extract_predicate predcclj.uj_val tms in
+          Coercion.inh_conv_coerces_to loc env !evdref predinst tycon)
+        !evdref tycon in
+      let predccl = (j_nf_evar sigma predcclj).uj_val in
+      [sigma, predccl]
   in
   List.map
-    (fun (sigma,dep,pred) ->
-      let (nal,pred) = build_initial_predicate dep names pred in
+    (fun (sigma,pred) ->
+      let (nal,pred) = build_initial_predicate arsign pred in
       sigma,nal,pred)
     preds
 
@@ -1698,15 +1801,33 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
   (* 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 arsign = extract_arity_signature env tomatchs tomatchl in
+  let preds = prepare_predicate loc typing_fun !evdref env tomatchs arsign tycon predopt in
 
   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) *)
 
-    let initial_pushed = List.map2 (fun tm na -> Pushed(tm,[],na)) tomatchs nal in
+    let out_tmt na = function NotInd (c,t) -> (na,c,t) | IsInd (typ,_,_) -> (na,None,typ) in
+    let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+
+    let typs =
+      List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
+
+    let dep_sign =
+      find_dependencies_signature
+        (list_make (List.length typs) true)
+        typs in
+
+    let typs' =
+      list_map3
+        (fun (tm,tmt) deps na ->
+          let deps = if not (isRel tm) then [] else deps in
+          ((tm,tmt),deps,na))
+        tomatchs dep_sign nal in
+
+    let initial_pushed = List.map (fun x -> Pushed x) typs' in
 
     (* A typing function that provides with a canonical term for absurd cases*)
     let typing_fun tycon env evdref = function