Un nouveau moteur pour Cases (phase 1)

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

2 files changed, 760 insertions, 1759 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b44077234d..ad02ce58bf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,23 +1,22 @@
 
-(* $Id$ *)
-
-open Pp
 open Util
 open Names
-open Sign
 open Generic
 open Term
 open Inductive
+open Environ
+open Sign
 open Reduction
-open Type_errors
 open Typeops
-open Environ
+open Type_errors
+
 open Rawterm
 open Retyping
-open Evarutil
 open Pretype_errors
+open Evarutil
 
 (*********************************************************************)
+(* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
 let mkExistential isevars env =
@@ -57,1760 +56,709 @@ let branch_scheme env isevars isrec i (mind,args as appmind) =
     norec_branch_scheme env isevars typc
 
 (************************************************************************)
+(*            Pattern-matching compilation (Cases)                      *)
+(************************************************************************)
 
-exception CasesError of env * type_error
-
-(* == General purpose functions == *)
-
-let starts_with_underscore id = 
- let s=string_of_id id in (String.get s 0)='_'
-
-let rec map_append_vect f v = 
-  let length = Array.length v in 
-  let rec map_rec i =
-    if i>=length then [] 
-    else (f v.(i))@ map_rec (i+1) 
-
-  in map_rec 0  
-
+(************************************************************************)
+(* Configuration, errors and warnings *)
 
+let substitute_alias = ref false
 
-(* behaves as lam_and_popl_named but receives an environment instead of a 
- *  dbenvironment
- *)
-let lam_and_pop_named env body acc_ids =
-  match env with
-    | [] -> error "lam_and_pop"
-    | (na,t)::tlenv ->
- 	let id = match na with
-	  | Anonymous -> next_ident_away (id_of_string "a") acc_ids
-	  | Name id -> id
-	in
-	(tlenv,DOP2(Lambda,body_of_type t,DLAM((Name id),body)),
-         (id::acc_ids))
-
-let lam_and_popl_named  n env t = 
-  let rec poprec = function
-    | (0, (env,b,_)) -> (env,b)
-    | (n, ([],_,_)) -> error "lam_and_popl"
-    | (n, (env,b,acc_ids)) -> poprec (n-1, lam_and_pop_named env b acc_ids)
-  in 
-  poprec (n,(env,t,[]))
+open Pp
 
-let elam_and_popl_named n env body =
-  let ENVIRON(sign,dbenv)=env in
-  let ndbenv,a = lam_and_popl_named n dbenv body
-  in ENVIRON(sign,ndbenv),a
+let error_bad_pattern_loc a = failwith "TODO1"
 
- 
-let lambda_name env (n,a,b) = 
-  mkLambda (named_hd env a n) a b
-let prod_name env (n,a,b) = 
-  mkProd (named_hd env a n) a b
+let mssg_may_need_inversion () =
+  [< 'sTR "This pattern-matching is not exhaustive.">]
 
+let mssg_this_case_cannot_occur () =
+  "This pattern-matching is not exhaustive."
 
-(* General functions on inductive types *)
+(* Utils *)
 
 let ctxt_of_ids ids =
   Array.of_list (List.map (function id -> VAR id) ids)
-
 let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids)
-
-let mutconstruct_of_rawconstructor c = 
-  mkMutConstruct (constructor_of_rawconstructor c)
 let inductive_of_rawconstructor c =
   inductive_of_constructor (constructor_of_rawconstructor c)
-let ith_constructor i mind =
-  mkMutConstruct (ith_constructor_of_inductive mind i)
-
-(* determines whether is a predicate or not *)
-let is_predicate ind_data = (ind_data.nrealargs > 0)
-
-(* === Closures imported from trad.ml to perform typing === *)
-
-type 'a trad_functions  = 
-  { pretype : trad_constraint -> env -> rawconstr -> unsafe_judgment;
-    isevars : 'a evar_defs
-    }
-
-type 'a lifted = int * 'a
-
-type lfconstr = constr lifted
-
-let lift_lfconstr n (s,c) = (s+n,c)
-
-(* Partial check on patterns *)
-let check_pat_arity env = function
-  | PatCstr (loc, (cstr_sp,ids as c), args, name) ->
-      let ity = inductive_of_rawconstructor c in
-      let nparams = mis_nparams (lookup_mind_specif ity env) in
-      let tyconstr =
-	type_of_constructor env Evd.empty (cstr_sp,ctxt_of_ids ids) in
-      let nb_args_constr = (nb_prod tyconstr) - nparams in
-	if List.length args <> nb_args_constr
-        then error_wrong_numarg_constructor_loc loc CCI cstr_sp nb_args_constr
-  | PatVar (_,_) -> ()
-
-(* Usage of this function should be avoided, because it requires that the
- * params are infered.
- *)
-let rec constr_of_pat isevars env = function
-    PatVar (_,Name id) -> VAR id
-  | PatVar (_,Anonymous) -> VAR (id_of_string "_")
-  (* invalid_arg "constr_of_pat"*)
-  | PatCstr(_,c,args,name) ->
-      let ity = inductive_of_rawconstructor c in
-      let mispec = Global.lookup_mind_specif ity in 
-      let nparams = mis_nparams mispec in
-      let c = mutconstruct_of_rawconstructor c in
-      let exl =
-	list_tabulate
-	  (fun _ ->
-	     fst (new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI))
-	  nparams in
-      applist(c, exl @ List.map (constr_of_pat isevars env) args)
-
-
-
-(* == Error messages == *)
-
-let warning_needs_dep_elim() =
-  warning
-"This pattern matching may need dependent elimination to be compiled.
-I will try, but if fails try again giving dependent elimination predicate."
-
-
-
-
-let mssg_may_need_inversion () =
-  [< 'sTR "This pattern-matching is not exhaustive.">]
-
-(* eta-expands the term t *)
-
-let rec eta_expand0 env sigma n c t =
-  match whd_betadeltaiota env sigma t with
-      DOP2(Prod,a,DLAM(na,b)) ->
-	DOP2(Lambda,a,DLAM(na,eta_expand0 env sigma (n+1) c b))
-   | _ -> applist (lift n c, rel_list 0 n)
-
-
-let rec eta_expand env sigma c t =
-  match whd_betadeltaiota env sigma c, whd_betadeltaiota env sigma t with
-   | (DOP2(Lambda,ta,DLAM(na,cb)), DOP2(Prod,_,DLAM(_,tb))) ->
-       DOP2(Lambda,ta,DLAM(na,eta_expand env sigma cb tb))
-   | (c, t) -> eta_expand0 env sigma 0 c t
-
-
-let eta_reduce_if_rel c =
-  match eta_reduce_head c with
-      Rel n -> Rel n
-    | _ -> c
-
-(* ===================================== *)
-(*        DATA STRUCTURES                *)
-(* ===================================== *)
-let push a s = a::s
-let push_lifted a s = (insert_lifted a)::s
-let pop = function (a::s) -> (a,s) | _ -> error "pop"
-
-(* dependencies: terms on which the type of patterns depends
-   patterns: list of patterns to analyse
-   rhs: right hand side of equations
-   Current pattern to analyse is placed in the top of patterns
-*)
-
-type rhs =
-    {private_ids:identifier list;
-     user_ids:identifier list;
-     subst:(identifier * constr) list;
-     rhs_lift:int;
-     it:rawconstr}
-
-type row = {dependencies : constr lifted list; 
-            patterns     : pattern list; 
-            rhs          : rhs}
-
-let row_current r = List.hd r.patterns
-let pop_row_current patts = List.tl patts
-
-
-(*---------------------------------------------------------------*
- *          Code for expansion of Cases macros                   *
- *---------------------------------------------------------------*)
-
-
-(* == functions for replacing variables except in patterns == *)
-(* (replace_var id t c) replaces for t all those occurrences of (VAR id) in c
- * that are not in patterns. It lifts t across binders.
- * The restriction is to avoid restoring parameters in patterns while treating
- * rhs.
- *)
-
-let subst_in_subst id t (id2,c) =
-   (id2,replace_vars [(id,make_substituend t)] c)
-
-let replace_var_nolhs id t rhs =
-  if List.mem id rhs.private_ids then
-    {rhs with
-	 subst = List.map (subst_in_subst id t) rhs.subst;
-         private_ids = list_except id rhs.private_ids}
-  else if List.mem id rhs.user_ids & not (List.mem_assoc id rhs.subst) then
-  {rhs with subst = (id,t)::List.map (subst_in_subst id t) rhs.subst}
-  else anomaly ("Found a pattern variables neither private nor user supplied: "
-		^(string_of_id id))
-
-
-
-
-  
-
-
-(* replaces occurrences of [(VAR id1)..(VAR idn)] respectively by t  in c *)
-let replace_lvar_nolhs lid t c =
-  List.fold_right (fun var c -> replace_var_nolhs var t c) lid c
-
-let rec global_vars_rawconstr env rhs =
-  rhs.user_ids@(ids_of_sign (get_globals env))
-
-(* ====================================================== *)
-(* Functions to absolutize alias names of as-patterns in  *)
-(*  a term                                                *)
-(* ====================================================== *)
-
-
-(* Rem: avant, lid étant dans l'autre sens, et replace_lvar_nolhs
-   utilise un fold_right. Comme je ne vois aucune dépendance entre des
-   différentes vars dans le terme value à substituer, l'ordre devrait
-   être indifférent [HH] *)
-
-let absolutize_hdname value rhs = function
-  | PatVar (_,Name id) -> replace_var_nolhs id value rhs
-  | PatVar (_,Anonymous) -> rhs
-  |  _ -> anomalylabstrm "absolutize_alias"
-                  [<'sTR "pattern should be a variable or an as-pattern">]
-
- 
-let pop_and_prepend_future lpatt patts = lpatt@(pop_row_current patts)
-
-type matrix = row list 
-
-(* info_flow allos to tag "tomatch-patterns" during expansion:
- * INH means that tomatch-pattern is given by the user
- * SYNT means that tomatch-pattern arises from destructuring a constructor
- *      (i.e. comes during top-down analysis of patterns)
- * INH_FIRST is used ONLY during dependent-Cases compilation. it tags the 
- *           first tomatch-pattern
- *)
-type info_flow = INH | SYNT | INH_FIRST
-
-
-
-(* If the case is non-dependent, the algorithm of compilation generates 
-   the predicate P of the analysis using la 0eme definition. When 
-   the case is dependent it should use the same strategy than rec.
-   For that terms to match are tagged with INH or SYNT so decide 
-   if pred should be inherited to branches or synthetised. 
-   While left to right analysis
-   of patterns the predicate is inherited, while top-down analysis of
-   patterns predicate is synthetised, by doing anonymous abstractions when
-   the non-dependent case is applied to an object of dependent type.
-*)
-
-type tomatch =
-  | IsInd of constr * inductive_summary
-  | MayBeNotInd of constr * constr
-
-let to_mutind env sigma c t =
-  try IsInd (c,try_mutind_of env sigma t)
-  with Induc -> MayBeNotInd (c,t)
-
-let term_tomatch = function
-    IsInd (c,_) -> c
-  | MayBeNotInd (c,_) -> c
-
-type general_data =
-    {case_dep : bool;
-     pred     : constr lifted;
-     deptm    : constr lifted list; 
-     tomatch  : (tomatch * info_flow) list;
-     mat      : matrix }
-
-let gd_current gd = List.hd gd.tomatch
-let pop_current gd = List.tl gd.tomatch
-
-let replace_gd_current cur gd =
-let tm = pop_current gd 
-in  {case_dep = gd.case_dep; pred=gd.pred; deptm=gd.deptm;
-    tomatch = cur:: tm; mat = gd.mat}
-
-
-let replace_gd_pred pred gd = 
- {case_dep = gd.case_dep; 
-  pred     = insert_lifted pred; 
-  deptm    = gd.deptm;
-  tomatch  = gd.tomatch;
-  mat      = gd.mat}
-
-
-
-let prepend_tomatch ltm gd =
- {case_dep = gd.case_dep; pred=gd.pred; deptm=gd.deptm;
-  tomatch = ltm@ gd.tomatch; mat = gd.mat}
-
-
-let pop_and_prepend_tomatch ltm gd =
-let tm = List.tl  gd.tomatch  
-in {case_dep= gd.case_dep; pred= gd.pred;   deptm = gd.deptm;
-    tomatch = ltm@tm;
-    mat = gd.mat}
-
-
 
-(* ========================================== *)
-(*    Lifiting operations for general data    *) 
-(* ========================================== *)
-
-(* == lifting db-indexes greater equal a base index in gd == *)
-(*  Ops. lifting indexes under b bindings (i.e. we lift only db-indexes
- *  that are >=  b
- *)
-
-(* lifts n the the indexes >= b of  row *)
-let lift_row n r = 
- {dependencies = List.map (lift_lfconstr n) r.dependencies;
-  patterns     = r.patterns; (* No Rel in patterns *)
-  rhs          = {r.rhs with rhs_lift = r.rhs.rhs_lift + n}}
-
-
-let lift_ind_data n md =
-  {fullmind=lift n md.fullmind;
-   mind=md.mind;
-   nparams=md.nparams;
-   nrealargs=md.nrealargs;
-   nconstr=md.nconstr;
-   params=List.map (lift n) md.params;
-   realargs=List.map (lift n) md.realargs;
-   arity=md.arity}
-
-
-let lift_tomatch n = function
-    IsInd(c,ind_data) -> IsInd (lift n c, lift_ind_data n ind_data)
-  | MayBeNotInd (c,t) -> MayBeNotInd (lift n c,lift n t)
-
-
-let lift_gd n {case_dep=b; pred=p; deptm=l; tomatch=tm; mat=m} =
-  {case_dep=b;
-   pred    = lift_lfconstr n p;
-   deptm   = List.map (lift_lfconstr n) l;
-   tomatch = List.map (fun (tm,i) -> (lift_tomatch n tm,i)) tm;
-   mat = List.map (lift_row n) m}
-
-
-(* == Ops lifting all db-indexes == *)
-
-(* pushes (na,t) to dbenv (that is a stack of (name,constr)  and lifts
- * tomach's dependencies, tomatch, pred and rhs in matrix 
- *)
+(* Environment management *)
 let push_rel_type sigma (na,t) env =
   push_rel (na,make_typed t (get_sort_of env sigma t)) env
 
 let push_rels vars env =
   List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars
 
-let push_and_liftn_gd n vl (env, gd) =
-  (List.fold_right (push_rel_type Evd.empty) vl env,  lift_gd n gd)
-
-let push_and_lift_gd       v   = push_and_liftn_gd 1 [v]
-
-(* if t not (x1:A1)(x2:A2)....(xn:An)t' then (push_and_lift_gdn n t (env,gd,l)
- * raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,t',gd')
- * where gd' is gd lifted n steps and l' is l lifted n steps
- *)
-
-let get_n_prod n t = 
-  let rec pushrec l = function
-      (0, t)                       -> (l,t)
-    | (n, DOP2(Prod,t,DLAM(na,b))) -> pushrec ((na,t)::l) (n-1, b)
-    | (n, DOP2(Cast,t,_))          -> pushrec l (n, t)
-    | (_, _) -> error "get_n_prod: Not enough products"
- in pushrec [] (n,t)
-
-
-let push_and_lift_gdn n t envgd =
-  let (vl,_) = get_n_prod n t in
-  let (nenv,ngd) = push_and_liftn_gd n vl envgd in
-    (nenv,ngd)
-
-
-let push_env_and_lift_gdn n dbenv_base dbenv gd a =
-  let rec pushrec base gd dbenv n = 
-    if n=0 then  base,gd
-    else 
-      try (match dbenv with 
-	     (na, t):: x  ->
-               let ndbenv,ngd = pushrec base gd x (n-1) in
-		 push_and_lift_gd  (na,t) (ndbenv, ngd)
-	     | _ -> assert false)
-      with UserError _ -> error "push_env_and_lift_gd"
-  in 
-  let (nbase,ngd) = pushrec dbenv_base gd (get_rels dbenv)  n in
-  (ngd,lift_lfconstr n a)
-
+(**********************************************************************)
+(* Structures used in compiling pattern-matching *)
+type 'a lifted = int * 'a
 
-(* == Ops. pushing  patterns to tomatch and lifting == *)
+let insert_lifted a = (0,a);;
 
-(* if t=(x1:P1)..(xn:Pn)Q behaves as push_and_lift_gd but if gd.patterns=patt 
- * then the resutling gd'.patterns = (Rel n)..(Rel 1)patt
- *)
+(* INVARIANT:
 
-let push_lpatt n t info (env,gd) =
-  let rec pushrec tl = function
-      (0, t, envgd) -> (tl,t,envgd)
-    | (n, DOP2(Prod,t,DLAM(na,b)), envgd)
-    -> pushrec (t::tl) (n-1, b, push_and_lift_gd (na,t) envgd)
-    | (n, DOP2(Cast,t,_), envgd) -> pushrec tl (n, t, envgd)
-    | (_, _, _) -> error "push_lpatt"
-  in let tl,body,(nenv,ngd) = pushrec [] (n,t,(env,gd)) in
-   let ntomatch =
-     list_map_i
-       (fun i t -> (to_mutind env Evd.empty (Rel i) (liftn (n-i+1) n t), info)) 1 tl
-   in body, (nenv,
-	     {ngd with tomatch=List.rev_append ntomatch ngd.tomatch})
+   The pattern variables of it are the disjoint union of [user_ids]
+   and the domain of [subst]. Non global VAR in the codomain of [subst] are
+   in private_ids.
+   The non pattern variables of it + the global VAR in the codomain of
+   [subst] are in others_ids
 
+*)
 
+type rhs =
+    { rhs_env    : env;
+      other_ids  : identifier list;
+      private_ids: identifier list;
+      user_ids   : identifier list;
+      subst      : (identifier * constr) list;
+      rhs_lift   : int;
+      it         : rawconstr }
 
-(* =============================================================== *)
+type pattern_source = DefaultPat of int | RegularPat
 
+type equation =
+    { dependencies : constr lifted list;
+      patterns     : pattern list; 
+      rhs          : rhs;
+      tag          : pattern_source }
 
-(* if tomatch=[Rel i1;...Rel in] of type 
-   [(Ti1 p1_bar u1_bar);..(Tij pj_bar uj_bar)] then it yields
-   [u1_bar;...uj_bar] 
-*)
-let find_depargs env tomatch =
-  let dep = function
-      (IsInd(c,{realargs=args}),_) -> args
-    | (MayBeNotInd (_,_),_) -> []
-  in list_map_append dep tomatch
+type matrix = equation list
 
+type tomatch_type =
+  | IsInd of inductive_summary
+  | NotInd of constr
 
-let rec hd_of_prodlam = function
-   DOP2(Prod,_,DLAM(_,c))   -> hd_of_prodlam c
- | DOP2(Lambda,t,DLAM(_,c)) -> hd_of_prodlam c
- | DOP2(Cast,c,t)     -> hd_of_prodlam t
- | DOPN(Evar _,_)   -> true
- | _ -> false
+type dependency_in_rhs = DepInRhs | NotDepInRhs
+type dependency_on_previous = DepOnPrevious | NotDepOnPrevious
+type dependency_status = dependency_on_previous * dependency_in_rhs
 
-let is_for_mlcase p = hd_of_prodlam p
+type pushed_attributes = (constr * tomatch_type) * dependency_in_rhs
+type topush_attributes = (name * tomatch_type) * dependency_status
 
-(* == functions for syntactic correctness test of patterns == *)
+type tomatch_status =
+  | Pushed of pushed_attributes lifted
+  | ToPush of topush_attributes
 
-let patt_are_var =
-  List.for_all
-    (fun r -> match row_current r with PatVar _ -> true |_ -> false)
+type tomatch_stack = tomatch_status list
 
+type predicate_signature =
+  | PrLetIn of (constr list * constr option) * predicate_signature
+  | PrProd of (bool * name * tomatch_type) * predicate_signature
+  | PrCcl of constr
 
-let check_pattern (ind_sp,_ as ind) row =
-  match row_current row with
-      PatVar (_,id) -> ()
-    | PatCstr (loc,(cstr_sp,ids),args,name) ->
-        if inductive_path_of_constructor_path cstr_sp <> ind_sp then
-	  error_bad_constructor_loc loc CCI (cstr_sp,ctxt_of_ids ids) ind
+(* A pattern-matching problem has the following form:
 
-let check_patt_are_correct ity mat = List.iter (check_pattern ity) mat 
+   env, isevars |- <pred> Cases tomatch of mat end
 
-(*The only variables that patterns can share with the environment are 
-  parameters of inductive definitions!. Thus patterns should also be 
-  lifted when pushing inthe context. *)
+  where tomatch is some sequence (t1  ... tn)
 
+  and mat is some matrix 
+   (p11 ... p1n -> rhs1)
+   (    ...            )
+   (pm1 ... pmn -> rhsm)
 
-(* == Function dealing with constraints in compilation of dep case == *)
+  Terms to match: there are 3 kinds of terms to match
 
-let xtra_tm = DOP0(XTRA("TMPATT"))
-let is_xtra_tm tm = match tm with DOP0(XTRA("TMPATT")) -> true |_ -> false
+  - initials terms are arbitrary terms given by user and typed in [env]
+  - to-push inherited terms are subterms, actually variables, obtained
+    from the top-down analysis of pattern, they are typed in [env]
+    enriched by the previous inherited terms to match and are still to be
+    pushed in env
+  - pushed inherited terms are variables refering to a variable in [env]
 
-(* represents the constraint cur=ci *)
-let build_constraint cur ci = DOP2(XTRA("CONSTRAINT"),cur,ci)
+  A variable inherited from a subpattern is not immediately pushed in
+  [env] because of possible dependencies from previous variables to match
 
-let top_constraint gd =
- match (extract_lifted gd.pred) with 
-  DOP2(Prod,(DOP2(XTRA("CONSTRAINT"),cur,ci)),_) -> true 
- |   _ -> false
+  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
+  variables present in the patterns. Therefore, they come with their
+  own [rhs_env] (actually it is the same as [env] except for the names
+  of variables).
 
-let destruct_constraint gd =
- match (extract_lifted gd.pred) with 
-  DOP2(Prod,(DOP2(XTRA("CONSTRAINT"),cur,ci)),bd) -> cur,ci,(lift (-1) bd)
- |   _ ->  anomalylabstrm "destruct_constraint" [<>]
+*)
+type 'a pattern_matching_problem =
+    { env      : env;
+      isevars  : 'a evar_defs;
+      pred     : predicate_signature option;
+      tomatch  : tomatch_stack;
+      mat      : matrix;
+      typing_function: trad_constraint -> env -> rawconstr -> unsafe_judgment }
 
+(************************************************************************)
+(* Utils *)
 
-let rec whd_constraint = function
-     DOP2(Prod,(DOP2(XTRA("CONSTRAINT"),_,_)),(DLAM(_,bd))) 
-          -> whd_constraint (lift (-1) bd)
-   | DOP2(Lambda,(DOP2(XTRA("CONSTRAINT"),_,_)),(DLAM(_,bd))) 
-           -> whd_constraint (lift (-1) bd)
-   | VAR(x)           -> (VAR x)
-   | DOPN(oper,cl)    -> DOPN(oper,Array.map whd_constraint  cl)
-   | DOPL(oper,cl)    -> DOPL(oper,List.map whd_constraint  cl)
-   | DOP1(oper,c)     -> DOP1(oper,whd_constraint  c)
-   | DOP2(oper,c1,c2) -> DOP2(oper,whd_constraint c1,whd_constraint c2)
-   | DLAM(na,c)       -> DLAM(na,whd_constraint  c)
-   | DLAMV(na,v)      -> DLAMV(na,Array.map whd_constraint  v)
-   | x                -> x
+let to_mutind env sigma t =
+  try IsInd (try_mutind_of env sigma t)
+  with Induc -> NotInd t
 
+let type_of_tomatch_type = function
+    IsInd ind_data -> ind_data.fullmind
+  | NotInd t -> t
 
-(* if next_pred = [d_bar:D_bar][h:(I~d_bar)]Q 
- * and bty = (y_bar:S_bar)(I~dep_ci)
- * and ci_params = (ci p_bar)
- * then it builds the next predicate containing the constraints in the correct
- * environment:
- * (y_bar:S_bar)
- *   (XTRA cur=(ci_param y_bar))->(next_pred dep_ci (ci_param dep_ci))
- *) 
+let current_pattern eqn =
+  match eqn.patterns with
+    | pat::_ -> pat
+    | [] -> anomaly "Empty list of patterns"
 
-(* PRE: gd.pred is a product correspondent to dependent elimination preidcate
- * productized (i.e. (d_bar:D_bar)(y:(I d_bar))Q )
- * It returns a product of the form
- * (s_bar:S_bar)Constraint->(whd_beta ([d_bar:D_bar][y:(I d_bar)]Q  dep_ci ci))
- * if info=INH then any constraints are generated
- *)
-let  insert_constraint next_env gd brty ((cur,info), ci_param) = 
-  let k = nb_prod brty in
-  let dbenv0,body = decompose_prod_n k brty in
-  let cur0 = lift k cur in
-  let cip0 = lift k ci_param in
-  let npred0 = lift k (extract_lifted gd.pred) in
-  let dep_ci = args_app body in
-  let cip1 = applist (cip0,(rel_list 0 k)) in 
-
-  let npred1 = to_lambda (Array.length dep_ci) npred0 in  
-
-  let ndbenv,bodypred,nk =
-    if Array.length dep_ci=1 (* type of cur is non-dependent *)  then 
-      dbenv0, appvect (npred1, dep_ci),k 
-    else   
-      let app_pred = appvect (npred1, dep_ci) in
-      if info = SYNT then  
-       	let c = build_constraint cur0 cip1 in
-       	(Anonymous,c)::dbenv0, (lift 1 app_pred), (k+1)
-
-      else dbenv0,app_pred,k  (* we avoid generating the constraint*) in 
- 
- (* we productize the constraint if some has been generated *)
-  prodn nk ndbenv (whd_beta next_env (* Hum *) Evd.empty bodypred)
-
-
-
-(********************************)
-(*  == compilation functions == *)
-(********************************)
-
-(* nbargs_iconstr is the number of arguments of the constructor i that are not
- * parameters. Current is the current value to substitute  "as" binders in
- * as-patterns 
- * About Expansion of as patterns: 
- * we absolutize alias names (x1..xn) in pattern in rhs by 
- * rhs [x1..xn <- gd.current]  if the type of current is not dep.
- * rhs [x1..xn <- (ci params lid)] otherwise
- * (in first case we share in second we rebuild the term)
- * Note: in the case of (VAR id) we use sharing whenver the type is non-dep
- * or we reconstruct the term when its dependent.
- * depcase tells if the current Case  to compile is dependent or not (this is
- * because during dependent compilation terms are always reconstructed and not
- * shared)
- * TODO: find a better criterion, or let the user choose...
- *)
-let ith_constructor_of_inductive (ind_sp,args) i = (ind_sp,i),args
-
-(* Le type d'un constructeur est syntaxiquement de conclusion I(...), pas *)
-(* de réduction à faire *)
-let constructor_numargs ind_data i =
-  let (ind_sp,args) = ind_data.mind in
-  nb_prod (type_of_constructor (Global.env()) Evd.empty ((ind_sp,i),args))
-  - ind_data.nparams
-
-type constructor_info =
-  {cstr_sp : constructor_path;
-   ctxt : constr array;
-   nargs : int;
-   args : (name * constr) list;
-   concl_realargs : constr list}
-     
-(* let realargs_of_constructor_concl ... *)
-
-(* On identifie ici toutes les variables/alias intervenant dans les [args]
-   des clauses filtrant le constructeur [cstr_sp] qui nous intéresse *)
-(*
-let alias_of_pattern = function
+let alias_of_pat = function
   | PatVar (_,name) -> name
   | PatCstr(_,_,_,name) -> name
 
-let merge_names na p (l,rhs) =
-  match na,alias_of_pattern p with
-  | Name id, Anonymous    -> na::l
-      tester si na n'existe pas déjà ailleurs dans rhs
-  | Anonymous, na    -> na::l, rhs
-  | Name id1, Name id2 -> id1::l, replace_lvar_nolhs id2 (VAR id1) rhs
-  
-let get_names_for_constructor_arg cstr_sp mat =
-  let egalize_names l row =
-    match row_current row with
-      | PatCstr(_,(cstr',_),largs,name) when cstr' = cstr_sp ->
-	  List.fold_right2 merge_names l largs ([],row.rhs)
-      | PatVar _ | PatCstr _ -> (l,row) in
-  let anonymous_list = list_tabulate (fun _ -> Anonymous) n in
-  List.fold_left egalize_names anonymous_list mat
-*)
+let remove_current_pattern eqn =
+  match eqn.patterns with
+    | _::pats -> { eqn with patterns = pats }
+    | [] -> anomaly "Empty list of patterns"
+
+let liftn_ind_data n depth md =
+  let mind' = 
+    let (ind_sp,ctxt) = md.mind in
+    (ind_sp, Array.map (liftn n depth) ctxt) in
+  { fullmind = liftn n depth md.fullmind;
+    mind = mind';
+    nparams = md.nparams;
+    nrealargs = md.nrealargs;
+    nconstr = md.nconstr;
+    params = List.map (liftn n depth) md.params;
+    realargs = List.map (liftn n depth) md.realargs;
+    make_arity = md.make_arity;
+    make_constrs = md.make_constrs }
+
+let liftn_tomatch_type n depth = function
+  | IsInd ind_data -> IsInd (liftn_ind_data n depth ind_data)
+  | NotInd t -> NotInd (liftn n depth t)
+
+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)
+
+let substn_many_ind_data cv depth md =
+  let mind' = 
+    let (ind_sp,ctxt) = md.mind in
+    (ind_sp, Array.map (substn_many cv depth) ctxt) in
+  { fullmind = substn_many cv depth md.fullmind;
+    mind = mind';
+    nparams = md.nparams;
+    nrealargs = md.nrealargs;
+    nconstr = md.nconstr;
+    params = List.map (substn_many cv depth) md.params;
+    realargs = List.map (substn_many cv depth) md.realargs;
+    make_arity = md.make_arity;
+    make_constrs = md.make_constrs }
+
+let substn_many_tomatch v depth = function
+  | IsInd ind_data -> IsInd (substn_many_ind_data v depth ind_data)
+  | NotInd t -> NotInd (substn_many v depth t)
+
+let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
+
+(**********************************************************************)
+(* Well-formedness tests *)
+(* Partial check on patterns *)
 
-let mychange_name_rel env current id =
-  match current with 
-      (Rel j) -> 
-	if starts_with_underscore id 
-	then env 
-	else change_name_rel env j id
-    |  _  -> env
-
-let submat depcase isevars env i ind_data params current mat =
-(* Futur...
-  let concl_realargs = realargs_of_constructor_concl ind_data i in
-  let constraints = matching concl_realargs ind_data.realargs in
+let check_constructor loc ((_,j as cstr_sp,ids),args) mind cstrs =
+  (* Check it is constructor of the right type *)
+  if inductive_path_of_constructor_path cstr_sp <> fst mind
+  then error_bad_constructor_loc loc CCI (cstr_sp,ctxt_of_ids ids) mind;
+  (* Check the constructor has the right number of args *)
+  let nb_args_constr = cstrs.(j-1).cs_nargs in 
+  if List.length args <> nb_args_constr
+  then error_wrong_numarg_constructor_loc loc CCI cstr_sp nb_args_constr
+
+let check_all_variables typ mat =
+  List.iter
+    (fun eqn -> match current_pattern eqn with
+       | PatVar (_,id) -> ()
+       | PatCstr (loc,_,_,_) -> error_bad_pattern_loc loc CCI typ)
+    mat
+
+(**********************************************************************)
+(* Functions to deal with matrix factorization *)
+let occur_rawconstr id =
+  let rec occur = function
+    | RRef (loc,RVar id) -> true
+    | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
+    | RBinder (loc,bk,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RCases (loc,prinfo,tyopt,tml,pl) ->
+	(occur_option tyopt) or (List.exists occur tml)
+	or (List.exists occur_pattern pl)
+    | ROldCase (loc,b,tyopt,tm,bv) -> 
+	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
+    | RRec (loc,fk,idl,tyl,bv) ->
+	(array_exists occur tyl) or
+	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
+    | RCast (loc,c,t) -> (occur c) or (occur t)
+    | (RSort _ | RHole _ | RRef _ ) -> false
+
+  and occur_pattern (idl,p,c) = not (List.mem id idl) & (occur c)
+
+  and occur_option = function None -> false | Some p -> occur p
+
+  in occur
+
+let occur_in_rhs na rhs =
+  match na with
+    | Anonymous -> false
+    | Name id -> occur_rawconstr id rhs.it
+
+let is_dep_patt eqn pat = occur_in_rhs (alias_of_pat pat) eqn.rhs
+
+let dependencies_in_rhs eqns =
+  let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in
+  let columns = matrix_transpose deps in
+  List.map (List.for_all ((=) true)) columns
+
+(* Introduction of an argument of the current constructor must be
+   delayed (flag DepOnPrevious) if it depends in the rhs and depends
+   on a previous variable of inductive type, or on a previous variable
+   already dependent *)
+
+let rec is_dep_on_previous n t = function
+  | ((_,IsInd _),_)::_ when dependent (Rel n) t -> DepOnPrevious
+  | ((_,NotInd _),(DepOnPrevious,DepInRhs))::_ 
+      when dependent (Rel n) t -> DepOnPrevious
+  | _::rest -> is_dep_on_previous (n+1) t rest
+  | [] -> NotDepOnPrevious
+
+let find_dependencies t prevlist is_dep_in_rhs =
+  if is_dep_in_rhs then (is_dep_on_previous 1 t prevlist,DepInRhs)
+  else (NotDepOnPrevious,NotDepInRhs)
+
+(******)
+
+(* A Pushed 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 terms to match and to push (dependent on t by definition)
+     must have (Rel depth) substituted by t and Rel's>depth lifted by n
+   - all pushed terms to match (non dependent on t by definition) must
+     be lifted by n
+
+  We start with depth=1
+
+  We delay lift for Pushed but not for ToPush (trop complexe !)
 *)
-  let nbargs_iconstr = constructor_numargs ind_data i in
-  let ci = ith_constructor i ind_data.mind in
-
-  let expand_row r =
-    let build_new_row subpatts name =
-      let lid = global_vars_rawconstr (context env) r.rhs in
-      let new_ids = get_new_ids nbargs_iconstr (id_of_string "t") lid in
-      let lpatt,largs = 
-	match subpatts with
-	  | None ->
-	      List.map (fun id -> PatVar (dummy_loc,Name id)) new_ids,
-	      List.map (fun id -> VAR id) new_ids
-	  | Some patts ->
-	      patts,
-              List.map (constr_of_pat isevars env) patts in
-      let value =
-	if (is_predicate ind_data) or depcase
-	then applist (ci, params@largs)
-        else current in
-      let vars = match name with Anonymous -> [] | Name id -> [id] in
-      { dependencies=r.dependencies;
-        patterns = pop_and_prepend_future lpatt r.patterns;
-        rhs = replace_lvar_nolhs vars value r.rhs } in
-
-    match row_current r with
-      | PatVar (_,name) ->
-	  let envopt = match name with
-	    | Anonymous -> None
-	    | Name id -> Some (mychange_name_rel env current id) in
-	  (envopt, [build_new_row None name])
-      | PatCstr(_,c,largs,alias) when mutconstruct_of_rawconstructor c = ci ->
-	(* Avant: il y aurait eu un problème si un des largs contenait
-   	   un "_". Un problème aussi pour inférer les params des
-   	   constructeurs sous-jacents, car on n'avait pas accès ici
-   	   aux types des sous-patterns. Ai donc remplacé le
-   	   "applist(c, params @ (List.map constr_of_pat largs))" par
-   	   un "applist (ci, params@(List.map (fun id -> VAR id) new_ids))"
-	   comme dans le cas PatVar, mais en créant des alias pour les
-	   sous-patterns. Au passage, ça uniformise le traitement maintenant
-	   fait par "build_new_row" *)
-	  let envopt = match alias with
-	    | Anonymous -> None
-	    | Name id -> Some (mychange_name_rel env current id) in
-	    (envopt,[build_new_row (Some largs) alias])
-      | PatCstr _ -> (None,[]) in
-
-  let lenv,llrows = List.split (List.map expand_row mat) in
-  let lrows = List.concat llrows in
-  let lsome = List.filter (fun op -> op <> None) lenv in
-  let rnenv = 
-    if lsome = [] then env 
-    else out_some (List.hd lsome)
-  in  rnenv, lrows
-
-
-type status =
-  | Match_Current of (constr * inductive_summary * info_flow) (* "(", ")" needed... *)
-  | Any_Tomatch | All_Variables
-  | Any_Tomatch_Dep | All_Variables_Dep | Solve_Constraint 
-
-let not_of_empty_type = function
-  | IsInd (c,{nconstr=nconstr}),_ -> nconstr <> 0
-  | MayBeNotInd (_,t),_ -> true  
-  (* Ici, on pourrait tester si t=?n et si oui unifier avec False ?? *)
-
-  
-let gdstatus env gd =
-  if top_constraint gd  then Solve_Constraint
-  else
-    match gd.tomatch with
-     [] -> if gd.case_dep then Any_Tomatch_Dep else Any_Tomatch
-  | (cj,info)::tl_tm ->
-   if gd.mat=[] then
-     if (List.for_all not_of_empty_type gd.tomatch)
-     then errorlabstrm "gdstatus" 
-       [< 'sTR "One should match a term in an empty inductive type"; 'fNL;
-	  'sTR "to get an empty list of pattern" >]
-     else (* to treat empty types *)
-       match cj with
-	   IsInd (current,ind_data) -> Match_Current (current,ind_data,info)
-	 | MayBeNotInd (current,t)  -> 
-	     if gd.case_dep then  All_Variables_Dep else  All_Variables
-   else
-     if (patt_are_var gd.mat)
-     then  if gd.case_dep then  All_Variables_Dep else  All_Variables
-     else
-       match cj with
-	   IsInd (current,ind_data) -> 
-	     if is_xtra_tm current then  Match_Current (current,ind_data,info)
-	     else
-	       (check_patt_are_correct ind_data.mind gd.mat;
-		Match_Current (current,ind_data,info))
-	 | MayBeNotInd (current,t) ->
-	     errorlabstrm "gdstatus" (error_case_not_inductive CCI env current t)
-
-
-(* J'ai remplace strip_outer_cast par whd_castapp. A revoir. PAPAGENO 01/1999
-let whd_cast = strip_outer_cast
-***********)
-
-let whd_cast = whd_castapp
-
-(* If S is the type of x and I that of y, then
- * solve_dep (x,S)(y,I) =
- * if S=(I u1..uj..un) and T=(I w1..wj..wn) where I has j parameters then
- *     u1=w1 &...& uj=wj & (solve u_j+1 w_j+1)& ..& (solve u_j+n w_j+n)
- *  else if S=(Rel i) and T=(Rel j) 
- *       else fail!
- * Note: this succeds only if uj+1...ur are all variables, otherwise 
- * inversion is needed.
- * WARNING!: here we compare using whd_cast is this enough or should we
- *  erase all cast before comparing??
- *)  
-let  rec solve_dep sigma env (x,t) (y,s)  = warning "solve_dep not implemented";[]
-(*
-  let rec solve_args  = function
-      [],[] -> []
-    | (e1::l1), (e2::l2) ->
-      	(match whd_cast e1 with
-           | (Rel i) -> ((Rel i), e2)::(solve_args (l1,l2))
-           | _ ->
-	       if  e1 = whd_cast e2 then (solve_args (l1,l2)) 
-               else error_needs_inversion CCI env x t)
-    | _ -> anomaly  "solve_dep"  in
-  try  
-    let (ityt,argst)= find_mrectype env sigma  t
-    and (itys,argss)= find_mrectype env sigma (hd_of_prod s)  in
-    if whd_cast ityt= whd_cast itys & (List.length argst = List.length argss)
-    then 
-      let nparams = mind_nparams ityt in
-      let (paramt,largst) = list_chop nparams argst
-      and (params,largss) = list_chop nparams argss in
-      if for_all2 eq_constr paramt params 
-      then  solve_args  (largst,largss) 
-      else anomalylabstrm "solve_dep" 
-          [<'sTR "mistake in the code building the branch!!" >]
-    else anomalylabstrm "solve_dep" 
-        [<'sTR "mistake in the code building the branch (pb:parameters)!">]
-  with Induc -> anomalylabstrm "solve_dep" 
-      [<'sTR "mistake in the code building the branch (pb: constructor)!">]
- *)
-
-let apply_subst subst dep =
-  let rec subst_term subst c = 
-    match subst with 
-      [] -> c
-    | (Rel i, t)::s -> 
-        if dependent (Rel i) c then
-          if i = 1 then subst1 t c  
-          else
-	    let lsubstituend =
-	      (List.rev (Array.to_list (rel_vect 0 (i-1))))@[t]
-            in  subst_term s (substl lsubstituend  c)
-        else  subst_term s c 
-    | _ -> assert false   in
-  let extr_subst_ins c =  insert_lifted (subst_term subst (extract_lifted c)) 
-  in   List.map extr_subst_ins dep 
-
-
-
-let solve_dependencies sigma env gd (current,ci)=
-  if gd.deptm = [] then gd.deptm
-  else
-    let (curv,curt) = destCast current in
-    let (civ,cit) = destCast ci in
-    try
-      let subst= solve_dep sigma env (curv,curt) (civ,cit) 
-      in apply_subst subst  gd.deptm
-    with UserError(a,b)-> errorlabstrm "solve_dependencies" b
-
-
-
-let rec substitute_dependencies c = function 
-    [], [] -> c
-  | (t::x), (var::y) -> 
-      (match (extract_lifted var) with
-	   (VAR id) as v  ->
-	     substitute_dependencies
-	       (replace_vars [(id,make_substituend (extract_lifted t))] c)
-	       (x,y)
-  	 | _ -> anomalylabstrm "substitute_dependencies" [<>] )
-  | _,_ -> anomalylabstrm "substitute_dependencies" 
-        [< 'sTR "Dep. tomatch mistmatch dependencies of patterns" >]
-
-
-
-(* depends .. env cur tm = true if the the type of some element of tm
- * depends on cur and false otherwise
- *) 
-(* I think that cur<>(Rel n) only during the first application of cc 
- * because later constructors in gd.tomatch are applied to variables
- *)
-let depends env cur tm =
-  let ENVIRON(sign,dbenv) = env  in
-  match cur with
-    (Rel n) ->
-      let (gamma2,_) = list_chop (n-1) dbenv in
-      let abs = lamn (n-1) (List.map (fun (na,t) -> na,body_of_type t) gamma2) mkImplicit
-      in dependent (Rel 1) abs 
-  | _ -> false
 
+let rec lift_subst_tomatch n (depth,ci as binder) = function
+  | [] -> []
 
+  (* By definition ToPush terms depend on the previous substituted tm *)
+  (* and they contribute to the environment (hence [depth+1]) *)
+  | ToPush ((na,t),info)::rest ->
+      let t' = liftn_tomatch_type n (depth+1) t in
+      let t'' = subst_tomatch binder t' in
+      ToPush ((na,t''), info)::(lift_subst_tomatch n (depth+1,ci) rest)
 
-let lift_ctxt  k env =
-  let ENVIRON(sign,dbenv) = env  in
-  let delta,_ = decompose_prod (lift k (prod_it mkImplicit dbenv)) in
-  ENVIRON(sign,delta)
-
-
-
-let split_ctxt j (ENVIRON(sign,db)) =
-  let db1,db2= list_chop j db in
-  (ENVIRON(sign,db1)), (ENVIRON(sign,db2))
-
-
-let prepend_db_ctxt (ENVIRON(sign1,db1)) (ENVIRON(sign2,db2)) =  
-  ENVIRON(sign1, db1@db2)
-
-
-
- 
-(* substitute_ctxt ci ENVIRON(sign, ([n1:U1]..[nj:Uj]))i = 
- *  substitutes ci by (Rel 1) in U1...Uj
- *)
-let subst1_ctxt  ci env =
-  let ENVIRON(sign,dbenv) = env  in
-  let delta,_ = decompose_prod (subst1 ci (prod_it mkImplicit dbenv)) in
-    ENVIRON(sign,delta)
-
-
-(* yields env if current pattern of first row is not a dummy var,
- * otherwise it undumize its identifier and renames the variable cur 
- * in context with the name of the current of the
- * first row.
- *)
-let rename_cur_ctxt env cur gd =
-  if gd.mat =[] then env
-  else
-    let r = List.hd gd.mat in
-    let current = row_current r in
-    match current with
-      PatVar (_,Name id) when not (starts_with_underscore id) ->
- 	mychange_name_rel env cur id
-    | _ -> env
-
-
-(* supposes that if |env|=n then the prefix of branch_env coincides with env
- * except for the name of db variables
- *)
-let common_prefix_ctxt env branch_env =
-  let (ENVIRON(sign,db))=env in
-  let (ENVIRON(_,branch_db)) = branch_env in 
-  let j = List.length db in
-  let rndb,_= list_chop j (List.rev branch_db)
-  in (ENVIRON(sign, List.rev  rndb))
+  (* By definition Pushed terms do not depend on previous terms to match *)
+  (* and are already pushed in the environment; *)
+  (* if all is correct, [c] has no variables < depth *)
+  | Pushed (lift,tm)::rest ->
+      Pushed (n+lift, tm)::(lift_subst_tomatch n binder rest)
 
+let subst_in_subst id t (id2,c) =
+   (id2,replace_vars [(id,make_substituend t)] c)
 
-let nf_ise_dependent sigma c t = dependent c (nf_ise1 sigma t)
+let replace_id_in_rhs id t rhs =
+  if List.mem id rhs.private_ids then
+    {rhs with
+	 subst = List.map (subst_in_subst id t) rhs.subst;
+         private_ids = list_except id rhs.private_ids}
+  else if List.mem id rhs.user_ids & not (List.mem_assoc id rhs.subst) then
+  {rhs with subst = (id,t)::List.map (subst_in_subst id t) rhs.subst}
+  else anomaly ("Found a pattern variables neither private nor user supplied: "
+		^(string_of_id id))
 
-let tm_depends current sigma ltm =
-  let rec dep_rec = function 
-      [] -> false
-    | (IsInd(tm,{params=params;realargs=args}),_)::ltm -> 
-	 List.exists (nf_ise_dependent sigma current) params
-	 or List.exists (nf_ise_dependent sigma current) args
-	 or (dep_rec ltm)
-    | (MayBeNotInd (tm,t),_)::ltm -> 
-	nf_ise_dependent sigma current t or (dep_rec ltm)
-  in dep_rec ltm
+let replace_name_in_rhs name c rhs =
+  match name with
+    | Anonymous -> rhs
+    | Name id -> replace_id_in_rhs id c rhs
 
+(* if [current] has type [I(p1...pn u1...um)] and we consider the case
+   of constructor [ci] of type [I(p1...pn u'1...u'm)], then the
+   default variable [name] is expected to have which type?
+   Rem: [current] is [(Rel i)] except perhaps for initial terms to match *)
 
+let rec pop_next_tomatchs acc = function
+  | ToPush((na,t),(NotDepOnPrevious,_ as deps))::l ->
+      pop_next_tomatchs (((na,t),deps)::acc) l
+  | ((ToPush(_,(DepOnPrevious,_)) | Pushed _)::_ | []) as l -> (acc,l)
 
+let expand_defaults pats current (name,eqn) =
+  { eqn with
+      patterns = pats @ eqn.patterns;
+      rhs = replace_name_in_rhs name current eqn.rhs }
 
-(* substitutes the current of the row by t in rhs. If the current of the row 
- * is an as-pattern, (p AS id) then it   expands recursively al as in such
- * patern by by  (expand rhs p)[id<- t]
- *)
-(* t is the current tomatch (used for expanding as-patterns) *)
-let subst_current value r =
-  {dependencies = r.dependencies;
-   patterns = pop_row_current r.patterns;
-   rhs = absolutize_hdname value r.rhs (row_current r)}
-
-
-(* t is the current tomatch (used for expanding as-patterns) *)
-let shift_current_dep value r  =
-  {dependencies = push (insert_lifted value) r.dependencies;
-   patterns = pop_row_current r.patterns;
-   rhs = absolutize_hdname value r.rhs (row_current r)}
-
-
-
-(* =========================================================================
- * the following functions determine the context of dependencies of a 
- * a vector of terms. They are useful to build abstractions wrt to dependencies
- * =========================================================================*)
-(* the type of c is (T p1..pn u1..um) (s.t. p1..pn are parameters of T
- *  and T:(x1:P1)...(xn:Pn)(y1:B1)..(ym:Bm)s) then
- *  [push_params env (c,(p1..pn,u1..um),_,_,_)] = 
- *     (env@[B1;..;Bm;(T (lift m p1)..(lift m pn) (Rel m)..(Rel 1))], 
- *      [u1;..um; c])
- *  in order to build later [y1:B1]..[ym:Bm](T p1'..pm' y1..ym)
- *  (where pi' = lift m pi)
- *)
+(************************************************************************)
+(* Some heuristics to get names for variables pushed in pb environment *)
 
-let arity_to_sign env ind_data =
-  let {params=params;arity=arity} = ind_data in
-  let arity0 = prod_applist arity params in
-  let sign,s = splay_prod env Evd.empty arity0 in
-  sign
-
-let abstracted_inductive sigma env ind_data =
-  let {mind=ity;params=params;nrealargs=m} = ind_data in
-  let asign = arity_to_sign env ind_data in
-  let sign = List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
-
-  let params0 = List.map (lift m) params in
-  let args0 = rel_list 0 m in
-  let t = applist (mkMutInd ity, params0@args0) in
-  let na = named_hd (Global.env()) t Anonymous in
-  (na,t)::sign, {ind_data with params=params0;realargs=args0}
-
-(* the type of current is (T p1..pn u1..um) (s.t. p1..pn are parameters of T
- *  and T:(x1:P1)...(xn:Pn)(y1:B1)..(ym:Bm)s) then
- * (tyenv_of_term tj) = [B1;..;Bm]
- *  in order to build later [y1:B1]..[ym:Bm]someterm
- *)
+let merge_names get_name =
+  List.map2 (fun obj na -> match na with
+	       | Anonymous -> get_name obj
+	       | _ -> na)
 
-let abstract_arity env res = function
-    IsInd (current,ind_data) ->
-      let sign = arity_to_sign env ind_data in
-      (ind_data.nrealargs, lam_it (lift ind_data.nrealargs res) sign)
-  | MayBeNotInd (_,_) -> 0,res
-
-
-
-(* =============================================== *)
-(*   for mlcase                                    *)
-(* =============================================== *)
-
-(* if ltmj=[j1;...jn] then this builds the abstraction
- *  [d1_bar:D1_bar] ...[dn_bar:Dn_bar](lift m pred)
- *  where di_bar are the dependencies of the type ji.uj_type and m is the sum
- *  of the lengths of d1_bar ... d1_n. 
- * The abstractions are not binding, because the predicate is properly lift
- *) 
-let abstract_pred_lterms env (pred,ltm) =
-  let rec abst = function
-      [] -> pred
-    | (tj::ltm) -> snd (abstract_arity env (abst ltm) tj)
-  in abst ltm
-
-let info_abstract_pred_lterms env (pred,ltm) =
-  let rec abst linfo = function
-      [] -> linfo,pred
-    | (tj::ltm) -> 
-     	let linfo,res = abst linfo ltm in
-     	let k,nres = abstract_arity env res tj in
-     	let info = if k=0 then SYNT else INH
-     	in (info::linfo),nres
-  in abst [] ltm
-
-
-(* if the type of cur is : (I p_bar d_bar) where d_bar are d_bar are 
- * dependencies, then this function builds (pred d_bar)
- * Precondition: pred has at least the same number of abstractions as d_bars 
- * length
- *)  
-let apply_to_dep env sigma pred = function
-  | IsInd (c,ind_data) -> whd_beta env sigma (applist (pred,ind_data.realargs))
-  | MayBeNotInd (c,t) -> pred
-
-(* == Special functions to deal with mlcase on objects of dependent types == *)
-
-(* analogue strategy as Christine's MLCASE *)
-let find_implicit_pred isevars ith_branch_builder env (current,ind_data,_) =
-  let {nconstr=nconstr;mind=mind;params=params;realargs=realargs} = ind_data in
-  let isrec = false in 
-  let rec findtype i = 
-    if i > nconstr then raise (CasesError (env, CantFindCaseType current))
-    else 
-      try
- 	(let expti = branch_scheme env isevars isrec i (mind,params) in
-       	let _,bri= ith_branch_builder i  in
-       	let fi = bri.uj_type in 
-       	let efit = nf_ise1 !isevars fi in 
-       	let pred =
-          Indrec.pred_case_ml_onebranch env !isevars isrec 
-            (current,(mind,params,realargs)) (i,bri.uj_val,efit) in
- 	if has_ise !isevars pred then error"isevar" else pred)
-      with UserError _ -> findtype (i+1)
-  in findtype 1  
-
-(* =============================================== *)
-(* Strategies for building elimination predicates  *)
-(* =============================================== *)
-(* we build new predicate p for elimination  
- * by 0-splitting (we use inheritance or synthesis) 
- *)
+let get_names env sign eqns =
+  let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in
+  (* If any, we prefer names used in pats, from top to bottom *)
+  let names2 = 
+    List.fold_right
+      (fun (pats,eqn) names -> merge_names alias_of_pat pats names)
+      eqns names1 in
+  (* Otherwise, we take names from the parameters of the constructor *)
+  let names3 = merge_names (fun (na,t) -> named_hd env t na) sign names2 in
+  (* Then we rename the base names to avoid conflicts *)
+  let allvars =
+    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.other_ids) [] eqns in
+  let names4,_ =
+    List.fold_left
+      (fun (l,avoid) na ->
+	 let id = next_name_away na avoid in
+      ((Name id)::l,id::avoid)) ([],allvars) names3 in
+  List.rev names4
 
-(* TODO: Display in the message the nested dependent pattern found *)
-let mssg_nested_dep_patt env mat =
-[< 'sTR "Compilation of Dependent Cases fails when there are";'cUT;
-   'sTR "nested patterns (in constructor form)  of dependent types."; 'cUT;
-   'sTR "Try to transform your expression in a sequence of Dependent Cases"; 
-   'cUT ; 'sTR "with simple patterns.">]
+(************************************************************************)
+(* Recovering names for variables pushed to the rhs' environment *)
 
+let rec recover_pat_names = function
+  | (_,t)::sign,p::pats -> (alias_of_pat p,t)::(recover_pat_names (sign,pats))
+  | [],_ -> []
+  | _,[] -> anomaly "Cases.recover_pat_names: Not enough patterns"
 
-let build_predicate isevars env (current,ind_data,info) gd =
-  let tl_tm = List.tl gd.tomatch in
-  let n = ind_data.nrealargs in
+let push_rels_eqn sign eqn =
+  let sign' = recover_pat_names (List.rev sign, eqn.patterns) in
+  {eqn with
+     rhs = {eqn.rhs with
+	      rhs_env = push_rels sign' eqn.rhs.rhs_env} }
 
-(* gd.pred has the form [deptm_1]..[deptm_r]P (as given by the user, this is
- * an invariant of the algorithm) 
- * then p = [deptm_1] ([demptm_2]...[deptm_r]P   val_deptm_2...val_dpetm_r)
- *      next_pred = [deptm_1]..[deptm_r]P
- *)
-  if not gd.case_dep then 
-(* this computations is done now in build_nondep_branch
- let abs = to_lambda nparams arityind in  
- let narity = whd_beta (applist (abs, params)) in
- let next_pred = if info=SYNT then lambda_ize n narity (extract_lifted gd.pred)                  else  extract_lifted gd.pred in
-*)
-    let next_pred = extract_lifted gd.pred  in
-    let (env0,pred0,_) = push_lam_and_liftl n [] next_pred [] in
-    let depargs= List.map (lift n) (find_depargs env tl_tm) in
-    let p = lamn n env0 (whd_beta env Evd.empty (applist (pred0,depargs)))
-    in (p,next_pred)
-
-  else begin
-    if n<>0 & info=SYNT then 
-      errorlabstrm "build_dep_predicate" (mssg_nested_dep_patt env gd.mat);
-    let npred = to_lambda (n+1) (extract_lifted gd.pred) 
-    in npred,npred
-  end
-  
+let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
 
 (*
-(* ity is closed *)  (* devrait être déplacé en tête *)
-let rec to_lambda_pred isevars ind_data n env prod =
-  if n=0 then prod 
-  else match prod with 
-    (DOP2(Prod,ty,DLAM(na,bd))) ->
-      mkLambda na ty 
-	(to_lambda_pred isevars ind_data (n-1) 
-(*	   (Mach.push_rel !isevars (na,ty) env) bd)*)
-	   (add_rel (na,outcast_type ty) env) bd)
-  | DOP2(Cast,c,_) -> to_lambda_pred isevars ind_data n env c
-  | _  -> error "to_lambda_unif"
-
+let substitute_rhs current pb =
+  if !substitute_alias then { pb with subst = current::pb.subst } else pb
 *)
-
-
-
-(* =================================== *)
-(*   Principal functions               *)
-(* =================================== *)
-let type_one_branch dep env sigma ind_data p im =
-  let i = im + 1 in
-  let {mind=ity;params=params;nparams=nparams} = ind_data in
-  let ct =
-    type_of_constructor env sigma (ith_constructor_of_inductive ity i) in
-  let rec typrec n c =
-    match whd_betadeltaiota env sigma c with 
-      | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2))
-      | x -> let lAV = destAppL(ensure_appl x) in
-             let (_,vargs) = array_chop (nparams+1) lAV in
-	     let c1 = appvect (lift n p,vargs) in
-	     if dep then 
-	       let co = ith_constructor i ind_data.mind in
-	       applist
-		 (c1,[applist(co,((List.map (lift n) params)@(rel_list 0 n)))])
-	     else c1
-  in 
-  typrec 0 (hnf_prod_applist env sigma "type_case" ct params)
-
-let find_type_case_branches sigma env dep ind_data p =
-  let {nconstr=nconstr;mind=ity;params=params} = ind_data in
-  Array.init nconstr (type_one_branch dep env sigma ind_data p)
-
-(*
-let my_norec_branch_scheme env sigma i ind_data =
-  let typc = type_inst_construct env sigma i (mutind_to_ind mind) in
-  let rec typrec n typc =
-    match whd_betadeltaiota env sigma typc with
-      DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,typrec (n+1) t))
-      | x -> let lAV = destAppL(ensure_appl x) in
-             let (_,vargs) = array_chop (nparams+1) lAV in
-             appvect (lift n p,vargs)
-  in
-  typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
-
-let find_type_case_branches isevars env (current,ind_data,_) p =
-  let {fullmind=ct;mind=ity;params=params;realargs=args} = ind_data in
-  if not (is_for_mlcase p) then
-
-    (* En attendant mieux ... *)
-    let pt = get_type_of env !isevars p in
-
-    let evalpt = nf_ise1 !isevars pt in
-    let (_,bty,_)= type_case_branches env !isevars ct evalpt p current
-    in bty
+let pop_pattern eqn = { eqn with patterns = List.tl eqn.patterns }
+
+(**********************************************************************)
+(* Functions to deal with elimination predicate *)
+
+(* Infering the predicate *)
+let prepare_unif_pb typ cs =
+  let n = cs.cs_nargs in
+  let (sign,p) = decompose_prod_n n typ in
+
+  (* We may need to invert ci if its parameters occur in p *)
+  let p' =
+    if noccur_bet 1 n p then lift (-n) p
+    else failwith "TODO4-1" in
+  let ci = applist
+	     (mkMutConstruct cs.cs_cstr, cs.cs_params@(rel_list (-n) n)) in
+
+  (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
+  (Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
+
+let infer_predicate typs cstrs ind_data =
+  let eqns = array_map2 prepare_unif_pb typs cstrs in
+
+  (* First strategy: no dependencies at all *)
+  let (cclargs,_,typn) = eqns.(ind_data.nconstr -1) in
+  if array_for_all (fun (_,_,typ) -> eq_constr typn typ) eqns
+  then
+    let (sign,_) = ind_data.make_arity ind_data.mind ind_data.params in
+    let pred = lam_it (lift (List.length sign) typn) sign in
+    (false,pred) (* true = dependent -- par défaut *)
   else
-    let build_branch i = my_norec_branch_scheme env isevars i ct in
-    let lbr = List.map build_branch (interval 1 ind_data.nconstr)
-    in  Array.of_list lbr
-*)
-
-(* if ityparam :(d_bar:D_bar)s
- * then we abstract the dependencies and the object building the non-binding
- * abstraction  [d_bar:D_bar][_:(I param d_bar)]body_br 
- *)
-
-(**************************************************************************)
+    failwith "TODO4-2"
+
+(* Propagation of user-provided predicate through compilation steps *)
+
+let lift_predicate n pred =
+  let rec liftrec k = function
+  | PrCcl ccl -> PrCcl (liftn n k ccl)
+  | PrProd ((dep,na,t),pred) ->
+	PrProd ((dep,na,liftn_tomatch_type n k t), liftrec (k+1) pred)
+    | PrLetIn ((args,copt),pred) ->
+	let args' = List.map (liftn n k) args in
+	let copt' = option_app (liftn n k) copt in
+	PrLetIn ((args',copt'), liftrec (k+1) pred) in
+  liftrec 1 pred
+
+let subst_predicate (args,copt) pred =
+  let sigma = match copt with
+    | None -> Array.map make_substituend (Array.of_list args)
+    | Some c -> Array.map make_substituend (Array.of_list (args@[c])) in
+  let rec substrec k = function
+    | PrCcl ccl -> PrCcl (substn_many sigma k ccl)
+    | PrProd ((dep,na,t),pred) ->
+	PrProd ((dep,na,substn_many_tomatch sigma k t), substrec (k+1) pred)
+    | PrLetIn ((args,copt),pred) ->
+	let args' = List.map (substn_many sigma k) args in
+	let copt' = option_app (substn_many sigma k) copt in
+	PrLetIn ((args',copt'), substrec (k+1) pred) in
+  substrec 0 pred
+
+let specialize_predicate_var = function
+  | PrProd _ | PrCcl _ ->
+     anomaly "specialize_predicate_var: a pattern-variable must be pushed"
+  | PrLetIn (tm,pred) -> subst_predicate tm pred
+
+let rec weaken_predicate n pred =
+  if n=0 then pred else match pred with
+    | PrLetIn _ | PrCcl _ ->
+		    anomaly "weaken_predicate: only product can be weakened"
+    | PrProd ((dep,_,IsInd ind_data),pred) ->
+	(* To make it more uniform, we apply realargs but they not occur! *)
+	let tm = (ind_data.realargs,if dep then Some (Rel n) else None) in
+	PrLetIn (tm, weaken_predicate (n-1)
+		   (lift_predicate ind_data.nrealargs pred))
+    | PrProd ((dep,_,NotInd t),pred) ->
+	let tm = ([],if dep then Some (Rel n) else None) in
+	PrLetIn (tm, weaken_predicate (n-1) pred)
+
+let rec extract_predicate = function
+  | PrProd ((_,na,t),pred) ->
+      mkProd na (type_of_tomatch_type t) (extract_predicate pred)
+  | PrLetIn ((args,Some c),pred) -> substl (args@[c]) (extract_predicate pred)
+  | PrLetIn ((args,None),pred) -> substl args (extract_predicate pred)
+  | PrCcl ccl -> ccl
+
+let abstract_predicate ind_data = function
+  | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
+  | PrLetIn ((_,copt),pred) ->
+      let asign,_ = ind_data.make_arity ind_data.mind ind_data.params in
+      let sign =
+	List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
+      let dep = copt<> None in
+      let sign' =
+	if dep then
+	  let ind = build_dependent_inductive ind_data in
+	  let na = named_hd (Global.env()) ind Anonymous in
+	  (na,ind)::sign
+	else sign in
+      (dep, lam_it (extract_predicate pred) sign')
+
+let specialize_predicate_match tomatchs cs = function
+  | PrProd _ | PrCcl _ ->
+     anomaly "specialize_predicate_match: a matched pattern must be pushed"
+  | PrLetIn ((args,copt),pred) ->
+      let argsi = Array.to_list cs.cs_concl_realargs in
+      let copti = option_app (fun _ -> build_dependent_constructor cs) copt in
+      let pred' = subst_predicate (argsi, copti) pred in
+      let pred'' = lift_predicate cs.cs_nargs pred' in
+      let dep = (copt <> None) in
+      List.fold_right
+	(* Ne perd-on pas des cas en ne posant pas true à la place de dep ? *)
+	(fun ((na,t),_) p -> PrProd ((dep,na,t),p)) tomatchs pred''
+
+let find_predicate p typs cstrs current ind_data =
+  let (dep,pred) =
+    match p with
+      | Some p -> abstract_predicate ind_data p
+      | None -> infer_predicate typs cstrs ind_data in
+  let typ = applist (pred, ind_data.realargs) in
+  if dep then (pred, applist (typ, [current]), dummy_sort)
+  else (pred, typ, dummy_sort)
 
-(* returns env,gd',args'  where:
- * if ltmj= e1...en then
- * we prepend (e1,INH_FIRST)(e2:INH)..(en,INH) to gd.tomatch (gd') and  
- * if not gd.case_dep  then env'=env and args'=[]
- *)
-let push_tomatch env gd ltm =
-  if not gd.case_dep  then  
-    env, prepend_tomatch (List.map (fun tm -> (tm,INH)) ltm) gd,[]
+(************************************************************************)
+(* Sorting equation 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 ind_data =
+  (* TODO *)
+  Constraints []
+
+let group_equations mind cstrs mat =
+  let brs = Array.create (Array.length cstrs) [] in
+  let dflt = ref [] in
+  let _ =
+    List.fold_left (* To be sure it's from bottom to top *)
+      (fun () eqn ->
+	 let rest = remove_current_pattern eqn in
+	 match current_pattern eqn with
+	   | PatVar (_,name) -> dflt := (name,rest) :: !dflt
+	   | PatCstr(loc,((ind_sp,i),ids as cstr),largs,alias) ->
+	       check_constructor loc (cstr,largs) mind cstrs;
+	       brs.(i-1) <- (largs,rest) :: brs.(i-1)) () mat in
+  (brs,!dflt)
+
+let pattern_status defaults eqns =
+  if eqns <> [] then RegularPat
   else
-    let rec push_rec gd args = function 
-      [] -> (gd,args)
-    | (IsInd (c,ind_data) as tm)::l ->
-	let {realargs=args} = ind_data in
-  	let tyargs = args@[c] in
-  	let ngd,resargs =  push_rec gd args l in
-  	(prepend_tomatch [(tm,INH)] ngd, (tyargs@resargs))
-    | (MayBeNotInd _)::l ->
-	errorlabstrm "push_tomatch" 
-	  [< 'sTR "Cases on terms of non inductive type is incompatible"; 
-	     'fNL; 'sTR "with dependent case analysis" >]
-  in
-    let ngd,nargs = push_rec gd [] (List.tl ltm) in
-    let fst_tm = (List.hd ltm) ,INH_FIRST in
-      (env, prepend_tomatch [fst_tm] ngd, nargs)
-
-
-(* ---------------------------------------------------------*)
-
-
+    let min =
+      List.fold_right
+	(fun (_,eqn) n -> match eqn with
+	   | {tag = DefaultPat i} when i<n -> i
+	   | _ -> n)
+	defaults 0 in
+    DefaultPat min
 
+(************************************************************************)
+(* Here start the pattern-matching compiling algorithm *)
 
-type dependency_option = DEP | NONDEP
-
-(* if ityparam :(d_bar:D_bar)s
- * then we abstract the dependencies and the object building the non-binding
- * abstraction  [d_bar:D_bar]body_br 
- *)
-let abstract_dep_generalized_args sigma env ind_data brj =
-  let m = ind_data.nrealargs in
-  let sign,_ = abstracted_inductive sigma env ind_data in
-  {uj_val = lam_it (lift (m+1) brj.uj_val) sign;
-   uj_type = prod_it (lift (m+1) brj.uj_type) sign;
-   uj_kind = brj.uj_kind}
-
-
-
-(* *)
-let check_if_may_need_dep_elim sigma current gd =
-    let tl_tm = List.tl gd.tomatch in
-      if (isRel current) & (tm_depends current sigma tl_tm)
-      then warning_needs_dep_elim()
-
-let rec cc trad env gd =
- match (gdstatus env gd) with
-   Match_Current (current,ind_data,info as cji) ->
-     if not gd.case_dep then 
-       (check_if_may_need_dep_elim !(trad.isevars) current gd;
-	match_current trad env cji gd)
-     else
-       match_current_dep trad env cji gd
- | All_Variables -> substitute_rhs trad  env gd
- | Any_Tomatch   -> build_leaf trad env gd 
-
-     (* for compiling dependent elimination *) 
- | All_Variables_Dep -> substitute_rhs_dep trad  env gd 
- | Any_Tomatch_Dep   -> build_leaf_dep     trad  env gd 
- | Solve_Constraint -> solve_constraint    trad  env gd 
-
-
-and solve_constraint trad env gd =
- let cur,ci,npred= destruct_constraint gd in
- let ngd =  {case_dep = gd.case_dep; 
-             pred = insert_lifted npred;
-             deptm = solve_dependencies !(trad.isevars) env gd (cur,ci);
-             tomatch = gd.tomatch;
-             mat = gd.mat}
- in cc trad env ngd
-
-
-and build_dep_branch trad env gd bty (current,ind_data,info) i =
- let sigma = !(trad.isevars) in
- let {mind=ity;params=params;realargs=args;nparams=nparams} = ind_data in
- let n =  (List.length args)+1 in
- let _,ty = decomp_n_prod env sigma nparams
-	      (type_of_constructor env sigma 
-		 (ith_constructor_of_inductive ity i)) in
- let l,_ = splay_prod env sigma ty in
- let lpatt = List.map (fun (na,ty) -> (to_mutind env sigma xtra_tm ty,SYNT)) l in
- let ngd =  pop_and_prepend_tomatch lpatt gd in
- let ci_param = applist (ith_constructor i ind_data.mind, params) in
-
- let rnnext_env0,next_mat = submat ngd.case_dep trad.isevars env i 
-                                    ind_data params current ngd.mat in
- let next_predicate = insert_constraint env ngd bty.(i-1) 
-                                       ((current,info),ci_param)  in
- let next_gd = {ngd with
-                  pred = insert_lifted next_predicate;
-                  mat = next_mat} in
- let brenv,body_br = cc trad rnnext_env0 next_gd in
- let branch =
-  if next_gd.tomatch = []
-  then body_br (* all the generalisations done in the elimination predicate 
-                * have been consumed *)
-  else let (_,nextinfo) = List.hd next_gd.tomatch  in
-  if nextinfo=SYNT then body_br (* there's no generalisation to consume *)
-   else (* consume generalisations in the elim pred. through abstractions *)
-   match (gdstatus rnnext_env0 next_gd) with
-     Match_Current _ | All_Variables | All_Variables_Dep -> body_br
-    | _ -> (* we abstract the generalized argument tomatch of 
-            * elimination predicate [d_bar:D_bar][_:(I param d_bar)]body_br 
-            *)
-        abstract_dep_generalized_args
-	  !(trad.isevars) rnnext_env0 ind_data body_br
- in
- let rnnext_env = common_prefix_ctxt (context env) brenv in
- rnnext_env,
- {uj_val=eta_reduce_if_rel branch.uj_val;uj_type=branch.uj_type;uj_kind=branch.uj_kind}
-                           
-(* build__nondep_branch ensures the invariant that elimination predicate in 
- * gd is always under the same form the user is expected to give it.
- * Thus, whenever an argument is destructed, for each
- * synthesed argument, the corresponding predicate is computed assuring
- * that the invariant.
- * Whenever we match an object u of type (I param t_bar),where I is a dependent
- * family of arity (x_bar:D_bar)s, in order to compile we
- *  1) replace the current element in gd by  (Rel 1) of type (I param x_bar)
- *     pushing to the environment env the new declarations  
- *     [x_bar : D_bar][_:(I param x_bar)]
- *  2) compile new gd in the environment env[x_bar : D_bar][_:(I param x_bar)]
- *     using the type (I param x_bar) to solve dependencies 
- *  3) pop the declarations [x_bar : D_bar][_:(I param x_bar)] from the
- *     environment by abstracting the result of compilation. We obtain a
- *     term ABST. Then apply the abstraction ABST to t_bar and u.
- *     The result is whd_beta (ABST t_bar u)
- *)
-
-and build_nondep_branch trad env gd next_pred bty
-  (current,ind_data,info as cji) i =
-  let {mind=ity;params=params;nparams=nparams;nrealargs=n} = ind_data in
-  let k = constructor_numargs ind_data i in
-
- (* if current is not rel, then we replace by rel so to solve dependencies *)
- let (nenv,ncurargs,ncur,ncurgd,npred,nbty) = 
-  if isRel current 
-   then (env, [], current, gd, (insert_lifted next_pred), bty.(i-1))
-   else
-     (* we push current and dependencies to environment *)
-     let sign,nind_data = abstracted_inductive !(trad.isevars) env ind_data in
-     let env1 = push_rels sign env in
-     let relargs = ind_data.realargs@[current] in
-     let nrelargs = n+1 in
-     (* we lift predicate and type branch w.r.t. to pushed arguments *) 
-     let curgd = lift_gd nrelargs gd in
-     let lpred = lift_lfconstr nrelargs (insert_lifted next_pred) in
-     (env1, relargs, (Rel 1), 
-      (replace_gd_current(IsInd(Rel 1,nind_data),info) curgd),
-      lpred, lift nrelargs bty.(i-1))     in
-
- let body,(next_env,ngd) = 
-   push_lpatt k nbty SYNT
-            (nenv,
-                 {case_dep= ncurgd.case_dep; 
-                  pred= npred;
-                  deptm = ncurgd.deptm;
-                  tomatch = List.tl ncurgd.tomatch;
-                  mat = ncurgd.mat}) in
- let nncur = lift k ncur in
- let lp = List.map (lift k) params in
- let ci = applist (ith_constructor i ind_data.mind, lp@(rel_list 0 k)) in 
-
- let rnnext_env0,next_mat=submat ngd.case_dep trad.isevars next_env i 
-                                 ind_data lp nncur ngd.mat in
-
- if next_mat = [] then
-      (* there is no row in the matrix corresponding to the ith constructor *)
-      errorlabstrm "build_nondep_branch" (mssg_may_need_inversion())
- else
-
-  let (linfo,npred) = 
-    let  dep_ci = args_app body in
-    let brpred = if (n=0 or Array.length dep_ci=0) then 
-                    (* elmination predicate of ngd has correct number
-                     * of abstractions *)
-                     extract_lifted ngd.pred 
-                 else whd_beta env !(trad.isevars) (appvect (extract_lifted ngd.pred, dep_ci)) in
-    let ciargs_patt =  List.map fst (fst (list_chop k ngd.tomatch)) in 
-           (*we put pred. under same format that should be given by user
-            * and set info to be INH, to indicate that dependecies have been
-            * generalized *)
-    let linfo,pred0 = info_abstract_pred_lterms env (brpred, ciargs_patt) 
-    in
-    (linfo,(insert_lifted pred0))
-  in
- 
- (* we change info of next current as current my pass from SYNT to INH
-  * whenver dependencies are generalized in elimination predicate *)
- let ntomatch = 
-  let synt_tomatch, inh_tomatch = list_chop k ngd.tomatch in
-  let nsynt_tomatch = List.map2 (fun info (tm,_) -> (tm,info))
-                            linfo synt_tomatch
-  in nsynt_tomatch @ inh_tomatch  in 
-   
- let next_gd = 
-  {case_dep = ngd.case_dep;
-   pred =  npred;
-   deptm = solve_dependencies !(trad.isevars) next_env ngd (nncur, ci);
-   tomatch = ntomatch ;
-   mat = next_mat}
- in
-
- let final_env, final_branch =
-  let brenv,body_br = cc trad rnnext_env0 next_gd in
-  let rnnext_env = common_prefix_ctxt (context next_env) brenv in
-  let branchenv,localenv = list_chop k (get_rels rnnext_env) in
-  let branchenv = List.map (fun (na,t) -> (na,incast_type t)) branchenv in
-  (* Avant ici, on nommait les Anonymous *)
-  let branchval = lam_it body_br.uj_val branchenv in
-  let branchtyp = prod_it body_br.uj_type branchenv in
-  ENVIRON(get_globals rnnext_env, localenv),
-  {uj_val=branchval;uj_type=branchtyp;uj_kind=body_br.uj_kind}
-
- in
-
- (* we restablish initial current by abstracting and applying  *)
- let p = List.length ncurargs  in
- let _,localenv = list_chop p (get_rels final_env) in
-  (* Avant ici, on nommait les Anonymous *)
- let app = substl ncurargs final_branch.uj_val in
- let typ = substl ncurargs final_branch.uj_type in
- ENVIRON(get_globals final_env, localenv),
- {uj_val = eta_reduce_if_rel app;
-  uj_type = typ;
-  uj_kind = final_branch.uj_kind}
-
-and match_current trad env (current,ind_data,info as cji) gd =
-  let {mind=ity;nparams=nparams;realargs=realargs;arity=arity;nconstr=nconstr} = ind_data in
-  let tl_tm = List.tl gd.tomatch in
-
-  (* we build new predicate p for elimination  *)
-  let (p,next_pred) =
-   build_predicate !(trad.isevars) env cji gd in
-
-  (* we build the branches *)
-  let bty = find_type_case_branches !(trad.isevars) env false ind_data p  in
-
-  let build_ith_branch gd = build_nondep_branch trad env gd 
-                               next_pred bty cji   in
-
-  let build_case ()=
-    let newenv,v =
-      match List.map (build_ith_branch gd) (interval 1 nconstr) with
-	  [] -> (*  nconstr=0 *)
-	   (context env),
-	  mkMutCaseA (ci_of_mind (mkMutInd ity)) 
-		    (eta_reduce_if_rel p) current [||]
-
-      | (bre1,f)::lenv_f as brl ->
-	let lfj = Array.of_list (List.map snd brl) in
-        let lf = Array.map (fun j -> j.uj_val) lfj in
-        let lft = Array.map (fun j -> j.uj_type) lfj in
-	let rec check_conv i =
-	  if i = nconstr then () else
-	    if not (Evarconv.the_conv_x_leq env trad.isevars lft.(i) bty.(i))
-	    then 
-	      let c = nf_ise1 !(trad.isevars) current
-	      and lfi = nf_betaiota env !(trad.isevars) (nf_ise1 !(trad.isevars) lft.(i)) in
-	      error_ill_formed_branch CCI env c i lfi (nf_betaiota env !(trad.isevars) bty.(i))
-	    else check_conv (i+1)
-	in
-	check_conv 0;
-        (common_prefix_ctxt (context env) bre1,
-         mkMutCaseA (ci_of_mind (mkMutInd ity))
-	   (eta_reduce_if_rel (nf_ise1 !(trad.isevars) p))
-	   current lf) in
-    newenv,
-    {uj_val = v;
-     uj_type = whd_beta env !(trad.isevars) (applist (p,realargs));
-     uj_kind = sort_of_arity env Evd.empty arity}
-
-  in
-(*
-  let build_mlcase () =
-    if nconstr=0 
-    then errorlabstrm "match_current" [< 'sTR "cannot treat ml-case">]
-    else 
-      let n = nb_localargs ind_data in
-      let np= extract_lifted gd.pred  in
-      let k = nb_lam np in
-      let (_,npred) = decompose_lam np in
-      let next_gd = {case_dep= gd.case_dep; 
-                     pred= insert_lifted npred;
-                     deptm = gd.deptm;
-                     tomatch = gd.tomatch;
-                     mat = gd.mat}
-      in
-      try (* we try to find out the predicate and recall match_current *)
-       (let ipred = find_implicit_pred trad.isevars
-		      (build_ith_branch  next_gd) 
-                      env cji in
-         (* we abstract with the rest of tomatch *)
-        let env0,bodyp = decompose_lam_n n ipred in
-         (*we put pred. under same format that should be given by user*)
-        let ipred0 = abstract_pred_lterms (bodyp, List.map fst tl_tm) in
-        let nipred = lamn n env0 ipred0  in
-        let explicit_gd = {gd with pred= insert_lifted nipred}
- 
-        in match_current trad env cji explicit_gd)
-
-      with UserError(_,s) -> errorlabstrm "build_mlcase" 
-                  [<'sTR "Not enough information to solve implicit Case" >] 
-
-  in if is_for_mlcase p then  build_mlcase ()
-     else *)  build_case ()
-
-
-and match_current_dep trad env (current,ind_data,info as cji) gd =
-  let sigma = !(trad.isevars) in 
-  let {mind=ity;params=params;realargs=args;nconstr=nconstr;arity=arity}=ind_data in
-
-  let nenv,ncurrent,ngd0=  
-    if info=SYNT then   (* we try to guess the type of current *)
-      if nb_prod (extract_lifted gd.pred) >0  then 
-        (* we replace current implicit by (Rel 1) *) 
-       	let nenv,ngd = push_and_lift_gdn 1 (extract_lifted gd.pred) (env,gd) in
-	let ngd0 = replace_gd_current
-		     (IsInd(Rel 1,lift_ind_data 1 ind_data),info) ngd
-       	in nenv,(Rel 1),ngd0 
-      else anomalylabstrm "match_current_dep" 
-          [<'sTR "sth. wrong with gd.predicate">]
-    else env,current,gd    (* i.e. current is typable in current env *)
-  in       
-
-  (* we build new predicate p for elimination  *)
-  let (p,next_pred) = build_predicate trad.isevars nenv cji ngd0  in
-
-  let np=whd_constraint p in
-  
-  (* we build the branches *)
-  let bty = find_type_case_branches !(trad.isevars) nenv true ind_data np in
-
-  let build_ith_branch env gd = build_dep_branch trad env gd bty cji in
-
-  let ngd1 = replace_gd_pred (to_prod (nb_lam next_pred) next_pred) ngd0 in
-
-  let build_dep_case () = 
-   let nenv,rescase,casetyp =
-    if info=SYNT then 
-      (*= builds [d_bar:D_bar][h:(I~d_bar)]<..>Cases current of lf end =*)
-
-      let lf = List.map
-		 (fun i -> 
-		    (snd (build_ith_branch nenv ngd1 i)).uj_val)
-                 (interval 1 nconstr) in
-      let case_exp =
- 	mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel np)
-	  current (Array.of_list lf) in
-      let (na,ty),_ = uncons_rel_env (context nenv) in
-      let rescase = lambda_name env (na,body_of_type ty,case_exp) in
-      let casetyp = whd_beta nenv !(trad.isevars) (applist (np,args)) in
-      (context nenv),rescase,casetyp
-    else  
-      if info = INH_FIRST then
-     (*= Consumes and initial tomatch so builds <..>Cases current of lf end =*)
-       let lf = List.map (fun i -> 
-			      (snd (build_ith_branch nenv ngd1 i)).uj_val)
-                  (interval 1 nconstr) in
-       let rescase = mkMutCaseA (ci_of_mind (mkMutInd ity)) 
-		 (eta_reduce_if_rel np) current (Array.of_list lf) in
-       let casetyp = whd_beta nenv !(trad.isevars) (applist (np,args)) in
-       (context nenv),rescase,casetyp
-
-      else  (* we treat an INH value *)
-       (* Consumes and initial tomatch abstracting that was generalized 
-        *  [m:T] <..>Cases current of lf end  *) 
-        let n = (List.length args)+1 in
-        let nenv1,ngd2 = push_and_lift_gdn n (extract_lifted gd.pred)
-			     (nenv, ngd1) in
-	let np1 = lift n np in
-        let lf = List.map (fun i -> 
-			       (snd (build_ith_branch nenv1 ngd2 i)).uj_val) 
-                       (interval 1 nconstr)   in
-        (* Now we replace the initial INH tomatch value (given by the user) 
-         * by (Rel 1) so to link it to the product. The instantiation of the
-         * this (Rel 1) by initial value will be done by the application 
-         *)
-        let case_exp =
-           mkMutCaseA (ci_of_mind (mkMutInd ity)) np1 (Rel 1) (Array.of_list lf) in
-        let nenv2,rescase = elam_and_popl_named n (context nenv1) case_exp in
-	let casetyp = whd_beta nenv1 !(trad.isevars) (applist (np,args@[(Rel 1)])) in
-        nenv2,rescase,casetyp
-
-   in
-   nenv,
-   {uj_val = rescase;
-    uj_type = casetyp;
-    uj_kind = sort_of_arity env Evd.empty arity}
-  in build_dep_case ()
-
-
-and bare_substitute_rhs trad tm_is_dependent env gd =
- let (cur,info),tm = pop gd.tomatch in
- let nenv = rename_cur_ctxt env (term_tomatch cur) gd in
- let npred = 
-   if gd.case_dep then gd.pred
-    else (* le prochain argument n'est pas filtrable (i.e. parce que les
-          *  motifs sont tous des variables ou parce qu'il n'y a plus de
-          *  motifs), alors npred est gd.pred *)    
-     let tmp_gd ={case_dep = gd.case_dep; pred = gd.pred; deptm = gd.deptm;
-                  tomatch = tm; 
-                  mat = List.map (subst_current (term_tomatch cur)) gd.mat} in
-     let pred0 = extract_lifted gd.pred in
-     let pred1 = apply_to_dep env !(trad.isevars) pred0 cur 
-     in insert_lifted pred1 in
-
-(* Je ne comprends pas à quoi sert la distinction dep ou pas car il n'y a ici
-   que des variables *)
- let ngd = (*if tm_is_dependent then
-              {case_dep = gd.case_dep; 
-               pred = npred;
-               deptm = push_lifted (term_tomatch cur) gd.deptm;
-               tomatch = tm; 
-               mat = List.map (shift_current_dep (term_tomatch cur)) gd.mat}  
-           else *){case_dep = gd.case_dep; 
-                 pred = npred;
-                 deptm = gd.deptm;
-                 tomatch = tm; 
-                 mat = List.map (subst_current (term_tomatch cur))  gd.mat}
-  in let brenv,res =  cc trad nenv ngd
-     in (common_prefix_ctxt (context nenv) brenv), res
-
-
-(* to preserve the invariant that elimination predicate is under the same
- * form we ask to the user, berfore substitution we compute the correct
- * elimination predicat whenver the argument is not inherited (i.e. info=SYNT)
- *)
-and substitute_rhs trad env gd =
- let (curj,info),tm = pop gd.tomatch in
- let nenv = rename_cur_ctxt env (term_tomatch curj) gd in
- let npred = 
-  match info with
-   SYNT -> (* we abstract dependencies in elimination predicate, to maintain
-             * the invariant, that gd.pred has always the correct number of
-             * dependencies *)
-            (*we put pred. under same format that should be given by user*)
-   (try let npred = abstract_pred_lterms env ((extract_lifted gd.pred),[curj])
-        in insert_lifted npred
-    with _ -> gd.pred )
-
-  | _          -> gd.pred  in
-
- let ngd = {gd with pred= npred} in
- let tm_is_dependent = depends (context env) (term_tomatch curj) tm 
- in bare_substitute_rhs trad tm_is_dependent env ngd
-
-
-and substitute_rhs_dep trad env gd =
- let (curj,info) = List.hd gd.tomatch in
- let (ty,v,npred) =
-   match get_n_prod 1 (extract_lifted gd.pred) with
-       ([_,ty as v], npred) -> (ty,v,npred)
-     | _ -> assert false in
- let nenv,ngd = push_and_lift_gd v (env,gd) in
- let ncur = (Rel 1) in
- let ntm = List.tl ngd.tomatch in
- let next_gd = {case_dep= gd.case_dep;
-                 pred = insert_lifted npred;
-                 deptm = ngd.deptm;
-                 tomatch = [(to_mutind env !(trad.isevars) ncur ty,info)]@ntm;
-                 mat= ngd.mat}  in
- let tm_is_dependent = dependent ncur npred in
- let nenv0,body= bare_substitute_rhs trad tm_is_dependent nenv next_gd in
- let (na,ty),nenv1 = uncons_rel_env nenv0 in
- let nbodyval = lambda_name env (na,incast_type ty,body.uj_val) in
- let nbodytyp = prod_name env (na,incast_type ty,body.uj_type) in
- let (nbodyval,nbodytyp) =
-   if info=INH_FIRST then
-     (applist(nbodyval,[term_tomatch curj]),
-      subst1 (term_tomatch curj) body.uj_type)
-   else (nbodyval,nbodytyp) in
- (nenv1, {uj_val=nbodyval;uj_type=nbodytyp;uj_kind=body.uj_kind})
-
-and build_leaf trad env gd =
-  match gd.mat with 
+(* No more patterns: typing the right-hand-side of equations *)
+let build_leaf pb =
+  match pb.mat with 
   | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
   | _::_::_ -> errorlabstrm "build_leaf" [<'sTR "Some clauses are redondant" >]
   | [row] ->
       let rhs = row.rhs in
+(*
       if List.length rhs.user_ids <> List.length rhs.subst then 
-	anomaly "Some user pattern variables has not been substituted";
+	anomaly "Some user pattern variable has not been substituted";
+*)
       if rhs.private_ids <> [] then
-	anomaly "Some private pattern variables has not been substituted";
-      let j = trad.pretype (mk_tycon (extract_lifted gd.pred)) env rhs.it in
-
-      let subst = List.map (fun id -> (id,make_substituend (List.assoc id rhs.subst))) rhs.user_ids in
-      let judge =
-      {uj_val = substitute_dependencies (replace_vars subst j.uj_val)
-		(gd.deptm, row.dependencies);
-       uj_type = substitute_dependencies (replace_vars subst j.uj_type)
-		 (gd.deptm, row.dependencies);
-       uj_kind = j.uj_kind} in
-      (context env),judge
-
-and build_leaf_dep trad env gd  = build_leaf trad env gd 
-
-
-
-(* Devrait être inutile et pris en compte par pretype 
-let check_coercibility isevars env ty indty =
-  if not (Evarconv.the_conv_x isevars env ty indty)
-  then errorlabstrm "productize" 
-    [< 'sTR "The type "; pTERMINENV (env,ty);
-       'sTR " in the Cases annotation predicate"; 'sPC;
-       'sTR "is not convertible to the inductive type"; 'sPC;
-       pTERM indty >]
-
-(* productize [x1:A1]..[xn:An]u builds (x1:A1)..(xn:An)u and uses
-   the types of tomatch to make some type inference *)
-let check_pred_correctness isevars env tomatchl pred =
-  let cook n = function
-    | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data))
-      -> (applist (mkMutInd ity,(List.map (lift n) params)
-		   @(rel_list 0 ind_data.nrealargs)),
-	  lift n (whd_beta env !isevars (applist (arity,params))))
-    | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent"
-  in
-  let rec checkrec n pred = function
-      |	[] -> pred
-      | tm::ltm ->
-	  let (ty1,arity) = cook n tm in
-	  let rec follow n (arity,pred) =
-            match (whd_betadeltaiota Evd.empty arity,
-		   whd_betadeltaiota !isevars pred) with
-		DOP2(Prod,ty2,DLAM(_,bd2)),DOP2(Lambda,ty,DLAM(na,bd)) ->
-		  check_coercibility isevars env ty2 ty;
-		  follow (n+1) (bd2,bd)
-	      | _ , DOP2(Lambda,ty,DLAM(na,bd)) ->
-		  check_coercibility isevars env ty1 ty;
-		  checkrec (n+1) bd ltm
-	  in follow n (arity,pred)
-  in checkrec 0 pred tomatchl
+	anomaly "Some private pattern variable has not been substituted";
+      let tycon = match pb.pred with
+	| None -> empty_tycon
+	| Some (PrCcl typ) -> mk_tycon typ
+	| Some _ -> anomaly "not all parameters of pred have been consumed" in
+      let j = pb.typing_function tycon rhs.rhs_env rhs.it in
+      let subst = (*List.map (fun id -> (id,make_substituend (List.assoc id rhs.subst))) rhs.user_ids *)[] in
+      {uj_val = replace_vars subst j.uj_val;
+       uj_type = replace_vars subst j.uj_type;
+       uj_kind = j.uj_kind}
+
+(* Building the sub-problem when all patterns are variables *)
+let shift_problem pb =
+  (* rhs have alr. the right env: we just have to pop a pattern & cook pred *)
+  {pb with
+     pred = option_app specialize_predicate_var pb.pred;
+     mat = List.map pop_pattern pb.mat }
+
+(* Building the sub-pattern-matching problem for a given branch *)
+let build_branch pb defaults current eqns const_info =
+  let names = get_names pb.env const_info.cs_args eqns in
+  let newpats =
+  if !substitute_alias then
+    List.map (fun na -> PatVar (dummy_loc,na)) names
+  else
+    List.map (fun _ -> PatVar (dummy_loc,Anonymous)) names in
+  let submatdef = List.map (expand_defaults newpats current) defaults in
+  let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
+  if submat = [] & submatdef = [] then error "Non exhaustive";
+  let typs = List.map2 (fun (_,t) na -> (na,t)) const_info.cs_args names in
+  let tomatchs =
+    List.fold_left2
+      (fun l (na,t) dep_in_rhs ->
+	 ((na,to_mutind pb.env !(pb.isevars) t),
+	  (find_dependencies t l dep_in_rhs))::l)
+      [] typs (dependencies_in_rhs eqns) in
+  let topushs = List.map (fun x -> ToPush x) tomatchs 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 =
+    applist
+      (mkMutConstruct const_info.cs_cstr, 
+       (List.map (lift const_info.cs_nargs) const_info.cs_params)
+       @(rel_list 0 const_info.cs_nargs)) in
+
+  (* We replace [(Rel 1)] by its expansion [ci] *)
+  let updated_old_tomatch =
+    lift_subst_tomatch const_info.cs_nargs (1,ci) pb.tomatch in
+  { pb with
+      tomatch = topushs@updated_old_tomatch;
+      mat = submat@submatdef;
+      pred = option_app (specialize_predicate_match tomatchs const_info) pb.pred }
+
+(**********************************************************************
+ INVARIANT:
+
+  pb = { env, subst, tomatch, mat, ...}
+  tomatch = list of Pushed (c:T) or ToPush (na:T) or Initial (c:T)
+
+  "Pushed" terms and types are relative to env
+  "ToPush" types are relative to env enriched by the previous terms to match
+
+  Concretely, each term "c" or type "T" comes with a delayed lift
+  index, but it works as if the lifting were effective.
 
 *)
-let build_expected_arity isdep env sigma tomatchl sort =
-  let cook n = function
-    | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data))
-      -> (applist (mkMutInd ity,(List.map (lift n) params)
-		   @(rel_list 0 ind_data.nrealargs)),
-	  lift n (whd_beta env sigma (applist (arity,params))))
-    | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent"
-  in
-  let rec buildrec n = function
-      |	[] -> sort
-      | tm::ltm ->
-	  let (ty1,arity) = cook n tm in
-	  let rec follow n arity =
-            match whd_betadeltaiota env sigma arity with
-		DOP2(Prod,ty2,DLAM(na,bd2)) ->
-		  DOP2(Prod,ty2,DLAM(na,follow (n+1) bd2))
-	      | _ ->
-		  if isdep then
-		  DOP2(Prod,ty1,DLAM(Anonymous,buildrec (n+1) ltm))
-		  else buildrec n ltm
-	  in follow n arity
-  in buildrec 0 tomatchl
-
-let rec productize  lam  = 
-  match strip_outer_cast lam with 
-    DOP2(Lambda,ty,DLAM(n,bd)) -> mkProd n ty (productize bd)
-  | x  -> x                      
-
-
-(* determines wether the multiple case is dependent or not. For that
- * the predicate given by the user is eta-expanded. If the result
- * of expansion is pred, then :
- * if pred=[x1:T1]...[xn:Tn]P and tomatchj=[|[e1:S1]...[ej:Sj]] then
- * if n= SUM {i=1 to j} nb_prod (arity Sj)
- *  then case_dependent= false
- *  else if n= j+(SUM (i=1 to j) nb_prod(arity Sj))
- *        then case_dependent=true
- *        else error! (can not treat mixed dependent and non dependent case
- *)
-let case_dependent env sigma loc predj tomatchj =
-  let nb_dep_ity = function
-      IsInd (_,ind_data) -> ind_data.nrealargs
-    | MayBeNotInd (c,t) -> errorlabstrm "case_dependent"
-	            (error_case_not_inductive CCI env c t)
-  in
-  let etapred = eta_expand env sigma predj.uj_val predj.uj_type in
-  let n = nb_lam etapred in
-  let _,sort = decomp_prod env sigma predj.uj_type in
-  let ndepv = List.map nb_dep_ity tomatchj in
-  let sum = List.fold_right (fun i j -> i+j)  ndepv 0 in
-  let depsum = sum + List.length tomatchj in
-  if n = sum then (false,build_expected_arity true env sigma tomatchj sort)
-  else if n = depsum
-  then (true,build_expected_arity true env sigma tomatchj sort)
-  else error_wrong_predicate_arity_loc loc CCI env etapred sum depsum
 
+(**********************************************************************)
+(* Main compiling descent *)
+let rec compile pb =
+  match pb.tomatch with
+    | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur
+    | (ToPush next)::rest -> compile_further pb next rest
+    | [] -> build_leaf pb
+
+and match_current pb (n,tm) =
+  let ((current,typ),info) = lift_tomatch n tm in
+  match typ with
+    | NotInd typ ->
+	check_all_variables typ pb.mat;
+	compile (shift_problem pb)
+    | IsInd ind_data ->
+	let cstrs = ind_data.make_constrs ind_data.mind ind_data.params in
+	let eqns,defaults = group_equations ind_data.mind cstrs pb.mat in
+	if array_for_all ((=) []) eqns
+	then compile (shift_problem pb)
+	else
+          let constraints = Array.map (solve_constraints ind_data) cstrs in
+	  let pbs =
+	    array_map2 (build_branch pb defaults current) eqns cstrs in
+	  let tags = Array.map (pattern_status defaults) eqns in
+	  let brs = Array.map compile pbs in
+	  let brvals = Array.map (fun j -> j.uj_val) brs in
+	  let brtyps = Array.map (fun j -> j.uj_type) brs in
+	  let (pred,typ,s) =
+	    find_predicate pb.pred brtyps cstrs current ind_data in
+	  { uj_val = mkMutCaseA (ci_of_mind (mkMutInd ind_data.mind (*,tags*)))
+		       (*eta_reduce_if_rel*) pred current brvals;
+	    uj_type = typ;
+	    uj_kind = s }
+
+and compile_further pb firstnext rest =
+  (* We pop as much as possible tomatch not dependent one of the other *)
+  let nexts,future = pop_next_tomatchs [firstnext] rest in
+  (* the next pattern to match is at the end of [nexts], it has ref (Rel n)
+     where n is the length of nexts *)
+  let sign = List.map (fun ((na,t),_) -> (na,type_of_tomatch_type t)) nexts in
+  let currents =
+    list_map_i
+      (fun i ((na,t),(_,rhsdep)) ->
+	 Pushed (insert_lifted ((Rel i, lift_tomatch_type i t), rhsdep)))
+      1 nexts in
+  let pb' = { pb with
+		env = push_rels sign pb.env;
+		tomatch = List.rev_append currents future;
+                pred= option_app (weaken_predicate (List.length sign)) pb.pred;
+		mat = List.map (push_rels_eqn sign) pb.mat } in
+  let j = compile pb' in
+  { uj_val = lam_it j.uj_val sign;
+    uj_type = prod_it j.uj_type sign;
+    uj_kind = j.uj_kind }
+
+
+(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
+substituer après par les initiaux *)
 
+(**************************************************************************)
+(* Preparation of the pattern-matching problem                            *)
 
 (* builds the matrix of equations testing that each row has n patterns
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in astterm *)
-let matx_of_eqns sigma env eqns n =
-  let build_row (ids,lpatt,rhs) =
-    List.iter (check_pat_arity env) lpatt;
-    { dependencies = []; 
-      patterns = lpatt;
-      rhs = {private_ids=[];subst=[];user_ids=ids;rhs_lift=0;it=rhs}}
-
-  in List.map build_row eqns
-
-
-
-let initial_gd cd npred matx =
-  { case_dep=cd;
-    pred=insert_lifted npred; 
-    deptm = []; 
-    tomatch = []; 
-    mat = matx }
-
-
+let matx_of_eqns env eqns =
+  let build_eqn (ids,lpatt,rhs) =
+    let rhs =
+      { rhs_env = env;
+	other_ids = ids@(ids_of_sign (get_globals (context env)));
+	private_ids = [];
+	user_ids = ids;
+	subst = [];
+	rhs_lift = 0;
+	it = rhs }
+    in { dependencies = [];
+	 patterns = lpatt;
+	 tag = RegularPat;
+	 rhs = rhs }
+  in List.map build_eqn eqns
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -1832,10 +780,6 @@ let rec find_row_ind = function
  * use the function above.
  *)
 
-let transpose mat =
-  List.fold_right (List.map2 (fun p c -> p::c)) mat
-    (if mat = [] then [] else List.map (fun _ -> []) (List.hd mat))
-
 exception NotCoercible
 
 let inh_coerce_to_ind isevars env ty tyi =
@@ -1854,99 +798,156 @@ let inh_coerce_to_ind isevars env ty tyi =
   else raise NotCoercible
 
 
-let coerce_row trad env row tomatch =
-  let j = trad.pretype mt_tycon env tomatch in
-  match find_row_ind row with
-      Some (cloc,(cstr,_ as c)) ->
-	(let tyi = inductive_of_rawconstructor c in
-	 try 
-	   let indtyp = inh_coerce_to_ind trad.isevars env j.uj_type tyi in
-	   IsInd (j.uj_val,try_mutind_of env !(trad.isevars) j.uj_type)
+let coerce_row typing_fun isevars env row tomatch =
+  let j = typing_fun empty_tycon env tomatch in
+  let t =
+    match find_row_ind row with
+	Some (cloc,(cstr,_ as c)) ->
+	  (let tyi = inductive_of_rawconstructor c in
+	   try 
+	     let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in
+	     IsInd (try_mutind_of env !isevars j.uj_type)
 	 with NotCoercible ->
 	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
 	   try
-	     let ind_data = try_mutind_of env !(trad.isevars) j.uj_type in
+	     let ind_data = try_mutind_of env !isevars j.uj_type in
 	     error_bad_constructor_loc cloc CCI
 	       (constructor_of_rawconstructor c) ind_data.mind
 	   with Induc ->
 	     error_case_not_inductive_loc
 	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
-    | None -> 
-	try IsInd (j.uj_val,try_mutind_of env !(trad.isevars) j.uj_type)
-	with Induc -> MayBeNotInd (j.uj_val,j.uj_type)
-
+      | None -> 
+	  try IsInd (try_mutind_of env !isevars j.uj_type)
+	  with Induc -> NotInd (j.uj_type)
+  in (j.uj_val,t)
 
-let coerce_to_indtype trad env matx tomatchl =
+let coerce_to_indtype typing_fun isevars env matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
-  List.map2 (coerce_row trad env) (transpose pats) tomatchl
-
-
-(* (mach_)compile_multcase:
- * The multcase that are in rhs are rawconstr
- * when we arrive at the leaves we call
- * trad.pretype that will  call compile recursively.
- * compile (<pred>Case e1..en end of ...)= ([x1...xn]t' e1...en)
- * where t' is the result of the translation. 
- * INVARIANT for NON-DEP COMPILATION: predicate in gd is always under the same
- * form we ask the user to write <..>.
- * Thus, during the algorithm, whenever the argument to match is inherited
- * (i.e. info<>SYNT) the elimination predicate in gd should have the correct
- * number of abstractions. Whenever the argument to match is synthesed we have
- * to abstract all the dependencies in the elimination predicate, before 
- * processing the tomatch argument. The invariant is thus preserved in the
- * functions build_nondep_branch y substitute_rhs.
- * Note: this function is used by trad.ml 
+  List.map2
+    (coerce_row typing_fun isevars env)
+    (matrix_transpose pats) tomatchl
+
+(***********************************************************************)
+(* preparing the elimination predicate if any                          *)
+
+let build_expected_arity isdep tomatchl sort =
+  let cook n = function
+    | _,IsInd ind_data ->
+	(build_dependent_inductive ind_data,
+	 fst (ind_data.make_arity ind_data.mind ind_data.params))
+    | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
+  in
+  let rec buildrec n = function
+    | [] -> sort
+    | tm::ltm ->
+	let (ty1,aritysign) = cook n tm in
+	let rec follow n = function
+	  | (na,ty2)::sign -> DOP2(Prod,lift n ty2,DLAM(na,follow (n+1) sign))
+	  | _ ->
+	      if isdep then DOP2(Prod,ty1,DLAM(Anonymous,buildrec (n+1) ltm))
+	      else buildrec n ltm
+	in follow n (List.rev aritysign)
+  in buildrec 0 tomatchl
+
+let build_initial_predicate isdep pred tomatchl =
+  let cook n = function
+    | _,IsInd ind_data ->
+	let args = List.map (lift n) ind_data.realargs in
+	if isdep then
+	  let ty = lift n (build_dependent_inductive ind_data) in
+	  (ind_data.nrealargs+1, (args,Some ty))
+	else
+	  (ind_data.nrealargs, (args,None))
+    | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
+  in
+  let rec buildrec n pred = function
+    | [] -> PrCcl pred
+    | tm::ltm ->
+	let (nargs,args) = cook n tm in
+	PrLetIn (args,buildrec (n+nargs) (snd(decompose_lam_n nargs pred)) ltm)
+  in buildrec 0 pred tomatchl
+
+let rec eta_expand0 env sigma n c t =
+  match whd_betadeltaiota env sigma t with
+      DOP2(Prod,a,DLAM(na,b)) ->
+	DOP2(Lambda,a,DLAM(na,eta_expand0 env sigma (n+1) c b))
+   | _ -> applist (lift n c, rel_list 0 n)
+
+
+let rec eta_expand env sigma c t =
+  match whd_betadeltaiota env sigma c, whd_betadeltaiota env sigma t with
+   | (DOP2(Lambda,ta,DLAM(na,cb)), DOP2(Prod,_,DLAM(_,tb))) ->
+       DOP2(Lambda,ta,DLAM(na,eta_expand env sigma cb tb))
+   | (c, t) -> eta_expand0 env sigma 0 c t
+
+(* determines wether the multiple case is dependent or not. For that
+ * the predicate given by the user is eta-expanded. If the result
+ * of expansion is pred, then :
+ * if pred=[x1:T1]...[xn:Tn]P and tomatchj=[|[e1:S1]...[ej:Sj]] then
+ * if n= SUM {i=1 to j} nb_prod (arity Sj)
+ *  then case_dependent= false
+ *  else if n= j+(SUM (i=1 to j) nb_prod(arity Sj))
+ *        then case_dependent=true
+ *        else error! (can not treat mixed dependent and non dependent case
  *)
+let case_dependent env sigma loc predj tomatchs =
+  let nb_dep_ity = function
+      (_,IsInd ind_data) -> ind_data.nrealargs
+    | (c,NotInd t) ->
+	errorlabstrm "case_dependent" (error_case_not_inductive CCI env c t)
+  in
+  let etapred = eta_expand env sigma predj.uj_val predj.uj_type in
+  let n = nb_lam etapred in
+  let _,sort = decomp_prod env sigma predj.uj_type in
+  let ndepv = List.map nb_dep_ity tomatchs in
+  let sum = List.fold_right (fun i j -> i+j)  ndepv 0 in
+  let depsum = sum + List.length tomatchs in
+  if n = sum then (false,build_expected_arity true tomatchs sort)
+  else if n = depsum
+  then (true,build_expected_arity true tomatchs sort)
+  else error_wrong_predicate_arity_loc loc CCI env etapred sum depsum
 
-let compile_multcase_fail trad vtcon env (predopt, tomatchl, eqns) =
-
- (* We build the matrix of patterns and right-hand-side *)
- let matx = matx_of_eqns !(trad.isevars) env eqns (List.length tomatchl) in
-
- (* We build the vector of terms to match consistently with the *)
- (* constructors found in patterns *)
- let tomatchj = coerce_to_indtype trad env matx tomatchl in
-
- (* We build the elimination predicate and check its consistency with *)
- (* the type of arguments to match *)
- let cd,npred =
-   match predopt with
-   | None ->
-       let finalres =
-	 match vtcon with
-	  | (_,(_,Some p)) -> p
-	  | _ -> let ty = mkCast dummy_sort dummy_sort in
-		 let (c,_) = new_isevar trad.isevars env ty CCI in c
-       in (false,abstract_pred_lterms env (finalres,tomatchj))
-   | Some pred ->
-     let loc = loc_of_rawconstr pred in
-     (* First call to exemeta to know if it is dependent *)
-     let predj1 = trad.pretype mt_tycon env pred in
-     let cdep,arity = case_dependent env !(trad.isevars) loc predj1 tomatchj in
-     (* We got the expected arity of pred and relaunch pretype with it *)
-     let predj = trad.pretype (mk_tycon arity) env pred in
-     let etapred = eta_expand env !(trad.isevars) predj.uj_val predj.uj_type in
-     if cdep then (cdep, productize etapred)
-     else (cdep,etapred) in
-
- let gdi = initial_gd cd npred matx in
-
- (* we push the terms to match to gd *)
- let env1,gd,args = push_tomatch env gdi tomatchj in
-
- (* Now we compile, abstract and reapply the terms tomatch *)
- let brenv,body = cc trad env1 gd in 
- let rnenv1 = common_prefix_ctxt (context env1) brenv in
- let k = List.length (get_rels (context env1)) - List.length (get_rels (context env)) in
- let abst = (* lamn k rnenv1 *) body.uj_val in
- let typ = body.uj_type in (* DEVRAIT ETRE INCORRECT *)
- let res = whd_beta env !(trad.isevars) (applist (abst, args)) in
-
- {uj_val=res;uj_type=typ;uj_kind=body.uj_kind}
-
-
-let compile_multcase (pretype,isevars) vtcon env loc macro =
- let trad = {pretype=(fun vtyc env -> pretype vtyc env); isevars = isevars} in
- try compile_multcase_fail trad vtcon env macro
- with CasesError (env,type_error) ->
-   raise (Stdpp.Exc_located (loc, TypeError(CCI,context env,type_error)))
+let prepare_predicate typing_fun isevars env tomatchs = function
+  | None -> None
+  | Some pred ->
+      let loc = loc_of_rawconstr pred in
+      (* First typing to know if it is dependent *)
+      let predj1 = typing_fun empty_tycon env pred in
+      let cdep,arity = case_dependent env !isevars loc predj1 tomatchs in
+      (* We got the expected arity of pred and relaunch pretype with it *)
+      let predj = typing_fun (mk_tycon arity) env pred in
+      let etapred = eta_expand env !isevars predj.uj_val predj.uj_type in
+      Some (build_initial_predicate cdep etapred tomatchs)
+
+(**************************************************************************)
+(* Main entry of the matching compilation                                 *)
+
+let compile_cases (typing_fun,isevars) vtcon env (predopt, tomatchl, eqns) =
+
+  (* We build the matrix of patterns and right-hand-side *)
+  let matx = matx_of_eqns env eqns in
+
+  (* We build the vector of terms to match consistently with the *)
+  (* constructors found in patterns *)
+  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+
+  (* We build the elimination predicate if any and check its consistency *)
+  (* with the type of arguments to match *)
+  let pred = prepare_predicate typing_fun isevars env tomatchs predopt in
+
+  let initial_pushed =
+    List.map (fun tm -> Pushed (insert_lifted (tm,NotDepInRhs))) tomatchs in
+
+  let pb =
+    { env      = env;
+      isevars  = isevars;
+      pred     = pred;
+      tomatch  = initial_pushed;
+      mat      = matx;
+      typing_function = typing_fun } in
+  
+  let j = compile pb in
+  
+  match vtcon with
+    | (_,(_,Some p)) -> Coercion.inh_conv_coerce_to env isevars p j
+    | _ -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9f121b1222..246f2135d5 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -17,9 +17,9 @@ val branch_scheme :
 
 (* Compilation of pattern-matching. *)
 
-val compile_multcase :
+val compile_cases :
   (trad_constraint -> env -> rawconstr -> unsafe_judgment)
-  * 'a evar_defs -> trad_constraint -> env -> loc ->
+  * 'a evar_defs -> trad_constraint -> env ->
     rawconstr option * rawconstr list *
     (identifier list * pattern list * rawconstr) list ->
     unsafe_judgment