Integrated obligations/eterm and program well-founded fixpoint building to toplevel/

The code is not called yet from there.

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

8 files changed, 4 insertions, 2637 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
deleted file mode 100644
index 3b740f1618..0000000000
--- a/plugins/subtac/subtac_cases.ml
+++ /dev/null
@@ -1,2015 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Cases
-open Errors
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Namegen
-open Declarations
-open Inductiveops
-open Environ
-open Sign
-open Reductionops
-open Typeops
-open Type_errors
-open Glob_term
-open Retyping
-open Pretype_errors
-open Evarutil
-open Evarconv
-open Subtac_utils
-
-(************************************************************************)
-(*            Pattern-matching compilation (Cases)                      *)
-(************************************************************************)
-
-(************************************************************************)
-(* Configuration, errors and warnings *)
-
-open Pp
-
-let mssg_may_need_inversion () =
-  str "Found a matching with no clauses on a term unknown to have an empty inductive type"
-
-(* Utils *)
-let make_anonymous_patvars =
-  list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous))
-
-(* Environment management *)
-let push_rels vars env = List.fold_right push_rel vars env
-
-(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
-   over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
-
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
-
-let rec regeneralize_index i k t = match kind_of_term t with
-  | Rel j when j = i+k -> mkRel (k+1)
-  | Rel j when j < i+k -> t
-  | Rel j when j > i+k -> t
-  | _ -> map_constr_with_binders succ (regeneralize_index i) k t
-
-type alias_constr =
-  | DepAlias
-  | NonDepAlias
-
-let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
-  { uj_val =
-      (match d with
-	| DepAlias -> mkLetIn (na,deppat,t,j.uj_val)
-	| NonDepAlias ->
-	    if (not (dependent (mkRel 1) j.uj_type))
-	      or (* A leaf: *) isRel deppat
-	    then
-	      (* The body of pat is not needed to type j - see *)
-	      (* insert_aliases - and both deppat and nondeppat have the *)
-	      (* same type, then one can freely substitute one by the other *)
-	      subst1 nondeppat j.uj_val
-	    else
-	      (* The body of pat is not needed to type j but its value *)
-	      (* is dependent in the type of j; our choice is to *)
-	      (* enforce this dependency *)
-	      mkLetIn (na,deppat,t,j.uj_val));
-    uj_type = subst1 deppat j.uj_type }
-
-(**********************************************************************)
-(* Structures used in compiling pattern-matching *)
-
-type rhs =
-    { rhs_env    : env;
-      avoid_ids  : identifier list;
-      it         : glob_constr;
-    }
-
-type equation =
-    { patterns     : cases_pattern list;
-      rhs          : rhs;
-      alias_stack  : name list;
-      eqn_loc      : loc;
-      used         : bool ref }
-
-type matrix = equation list
-
-(* 1st argument of IsInd is the original ind before extracting the summary *)
-type tomatch_type =
-  | IsInd of types * inductive_type
-  | NotInd of constr option * types
-
-type tomatch_status =
-  | Pushed of ((constr * tomatch_type) * int list)
-  | Alias of (constr * constr * alias_constr * constr)
-  | Abstract of rel_declaration
-
-type tomatch_stack = tomatch_status list
-
-(* The type [predicate_signature] types the terms to match and the rhs:
-
-   - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]),
-     if dep<>Anonymous, the term is dependent, let n=|names|, if
-     n<>0 then the type of the pushed term is necessarily an
-     inductive with n real arguments. Otherwise, it may be
-     non inductive, or inductive without real arguments, or inductive
-     originating from a subterm in which case real args are not dependent;
-     it accounts for n+1 binders if dep or n binders if not dep
-   - [PrProd] types abstracted term ([Abstract]); it accounts for one binder
-   - [PrCcl] types the right-hand side
-   - Aliases [Alias] have no trace in [predicate_signature]
-*)
-
-type predicate_signature =
-  | PrLetIn of (name list * name) * predicate_signature
-  | PrProd of predicate_signature
-  | PrCcl of constr
-
-(* We keep a constr for aliases and a cases_pattern for error message *)
-
-type alias_builder =
-  | AliasLeaf
-  | AliasConstructor of constructor
-
-type pattern_history =
-  | Top
-  | MakeAlias of alias_builder * pattern_continuation
-
-and pattern_continuation =
-  | Continuation of int * cases_pattern list * pattern_history
-  | Result of cases_pattern list
-
-let start_history n = Continuation (n, [], Top)
-
-let feed_history arg = function
-  | Continuation (n, l, h) when n>=1 ->
-      Continuation (n-1, arg :: l, h)
-  | Continuation (n, _, _) ->
-      anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
-  | Result _ ->
-      anomaly "Exhausted pattern history"
-
-(* This is for non exhaustive error message *)
-
-let rec glob_pattern_of_partial_history args2 = function
-  | Continuation (n, args1, h) ->
-      let args3 = make_anonymous_patvars (n - (List.length args2)) in
-      build_glob_pattern (List.rev_append args1 (args2@args3)) h
-  | Result pl -> pl
-
-and build_glob_pattern args = function
-  | Top -> args
-  | MakeAlias (AliasLeaf, rh) ->
-      assert (args = []);
-      glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
-  | MakeAlias (AliasConstructor pci, rh) ->
-      glob_pattern_of_partial_history
-	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
-
-let complete_history = glob_pattern_of_partial_history []
-
-(* This is to build glued pattern-matching history and alias bodies *)
-
-let rec simplify_history = function
-  | Continuation (0, l, Top) -> Result (List.rev l)
-  | Continuation (0, l, MakeAlias (f, rh)) ->
-      let pargs = List.rev l in
-      let pat = match f with
-	| AliasConstructor pci ->
-	    PatCstr (dummy_loc,pci,pargs,Anonymous)
-	| AliasLeaf ->
-	    assert (l = []);
-	    PatVar (dummy_loc, Anonymous) in
-      feed_history pat rh
-  | h -> h
-
-(* Builds a continuation expecting [n] arguments and building [ci] applied
-   to this [n] arguments *)
-
-let push_history_pattern n current cont =
-  Continuation (n, [], MakeAlias (current, cont))
-
-(* A pattern-matching problem has the following form:
-
-   env, isevars |- <pred> Cases tomatch of mat end
-
-  where tomatch is some sequence of "instructions" (t1  ... tn)
-
-  and mat is some matrix
-   (p11 ... p1n -> rhs1)
-   (    ...            )
-   (pm1 ... pmn -> rhsm)
-
-  Terms to match: there are 3 kinds of instructions
-
-  - "Pushed" terms to match are typed in [env]; these are usually just
-    Rel(n) except for the initial terms given by user and typed in [env]
-  - "Abstract" instructions means an abstraction has to be inserted in the
-    current branch to build (this means a pattern has been detected dependent
-    in another one and generalisation is necessary to ensure well-typing)
-  - "Alias" instructions means an alias has to be inserted (this alias
-    is usually removed at the end, except when its type is not the
-    same as the type of the matched term from which it comes -
-    typically because the inductive types are "real" parameters)
-
-  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).
-
-*)
-type pattern_matching_problem =
-    { env      : env;
-      isevars  : Evd.evar_map ref;
-      pred     : predicate_signature option;
-      tomatch  : tomatch_stack;
-      history  : pattern_continuation;
-      mat      : matrix;
-      caseloc  : loc;
-      casestyle: case_style;
-      typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment }
-
-(*--------------------------------------------------------------------------*
- * A few functions to infer the inductive type from the patterns instead of *
- * checking that the patterns correspond to the ind. type of the            *
- * destructurated object. Allows type inference of examples like            *
- *  match n with O => true | _ => false end                                 *
- *  match x in I with C => true | _ => false end                            *
- *--------------------------------------------------------------------------*)
-
-(* Computing the inductive type from the matrix of patterns *)
-
-(* We use the "in I" clause to coerce the terms to match and otherwise
-   use the constructor to know in which type is the matching problem
-
-   Note that insertion of coercions inside nested patterns is done
-   each time the matrix is expanded *)
-
-let rec find_row_ind = function
-    [] -> None
-  | PatVar _ :: l -> find_row_ind l
-  | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
-
-let inductive_template isevars env tmloc ind =
-  let arsign = get_full_arity_sign env ind in
-  let hole_source = match tmloc with
-    | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
-    | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
-   let (_,evarl,_) =
-    List.fold_right
-      (fun (na,b,ty) (subst,evarl,n) ->
-	match b with
-        | None ->
-	    let ty' = substl subst ty in
-	    let e = e_new_evar isevars env ~src:(hole_source n) ty' in
-	    (e::subst,e::evarl,n+1)
-	| Some b ->
-	    (b::subst,evarl,n+1))
-      arsign ([],[],1) in
-   applist (mkInd ind,List.rev evarl)
-
-
-(************************************************************************)
-(* Utils *)
-
-let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars =
-  e_new_evar isevars env ~src:src (new_Type ())
-
-let evd_comb2 f isevars x y =
-  let (evd',y) = f !isevars x y in
-  isevars := evd';
-  y
-
-let context_of_arsign l =
-  let (x, _) = List.fold_right
-    (fun c (x, n) ->
-      (lift_rel_context n c @ x, List.length c + n))
-    l ([], 0)
-  in x
-
-(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
-
-let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
-  let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
-  let subst, len =
-    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
-      let signlen = List.length sign in
-	match kind_of_term tm with
-	  | Rel n when dependent tm c
-		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
-				      maybe some variable in its type appears in the tycon. *) ->
-	      (match tmtype with
-	      | NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
-	      | IsInd (_, IndType(indf,realargs)) ->
-		  let subst =
-		    if dependent tm c && List.for_all isRel realargs
-		    then (n, 1) :: subst else subst
-		  in
-		    List.fold_left
-		      (fun (subst, len) arg ->
-			match kind_of_term arg with
-			| Rel n when dependent arg c ->
-			    ((n, len) :: subst, pred len)
-			| _ -> (subst, pred len))
-		      (subst, len) realargs)
-	  | _ -> (subst, len - signlen))
-      ([], nar) tomatchs arsign
-  in
-  let rec predicate lift c =
-    match kind_of_term c with
-      | Rel n when n > lift ->
-	  (try
-	      (* Make the predicate dependent on the matched variable *)
-	      let idx = List.assoc (n - lift) subst in
-		mkRel (idx + lift)
-	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
-	      mkRel (n + nar))
-      | _ ->
-	  map_constr_with_binders succ predicate lift c
-  in
-    try
-      (* The tycon may be ill-typed after abstraction. *)
-      let pred = predicate 0 c in
-      let env' = push_rel_context (context_of_arsign arsign) env in
-	ignore(Typing.sort_of env' evm pred); pred
-    with _ -> lift nar c
-
-
-let inh_coerce_to_ind isevars env ty tyi =
-  let expected_typ = inductive_template isevars env None tyi in
-     (* devrait être indifférent d'exiger leq ou pas puisque pour
-        un inductif cela doit être égal *)
-  let _ = e_cumul env isevars expected_typ ty in ()
-
-let unify_tomatch_with_patterns isevars env loc typ pats =
-  match find_row_ind pats with
-    | None -> NotInd (None,typ)
-    | Some (_,(ind,_)) ->
-	inh_coerce_to_ind isevars env typ ind;
-	try IsInd (typ,find_rectype env ( !isevars) typ)
-	with Not_found -> NotInd (None,typ)
-
-let find_tomatch_tycon isevars env loc = function
-  (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_) -> mk_tycon (inductive_template isevars env loc ind)
-  | None -> empty_tycon
-
-let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_glob_constr tomatch) in
-  let tycon = find_tomatch_tycon isevars env loc indopt in
-  let j = typing_fun tycon env tomatch in
-  let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in
-  isevars := evd;
-  let typ = nf_evar ( !isevars) j.uj_type in
-  let t =
-    try IsInd (typ,find_rectype env ( !isevars) typ)
-    with Not_found ->
-      unify_tomatch_with_patterns isevars env loc typ pats in
-  (j.uj_val,t)
-
-let coerce_to_indtype typing_fun isevars env matx tomatchl =
-  let pats = List.map (fun r ->  r.patterns) matx in
-  let matx' = match matrix_transpose pats with
-    | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
-    | m -> m in
-  List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
-
-
-
-let adjust_tomatch_to_pattern pb ((current,typ),deps) =
-  (* Ideally, we could find a common inductive type to which both the
-     term to match and the patterns coerce *)
-  (* In practice, we coerce the term to match if it is not already an
-     inductive type and it is not dependent; moreover, we use only
-     the first pattern type and forget about the others *)
-  let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
-  let typ =
-    try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ)
-    with Not_found -> NotInd (None,typ) in
-  let tomatch = ((current,typ),deps) in
-  match typ with
-  | NotInd (None,typ) ->
-      let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
-      (match find_row_ind tm1 with
-	| None -> tomatch
-	| Some (_,(ind,_)) ->
-	    let indt = inductive_template pb.isevars pb.env None ind in
-	    let current =
-	      if deps = [] & isEvar typ then
-	      (* Don't insert coercions if dependent; only solve evars *)
-		let _ = e_cumul pb.env pb.isevars indt typ in
-		current
-	      else
-		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.isevars (make_judge current typ) indt).uj_val in
-	    let sigma =  !(pb.isevars) in
-	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
-	    ((current,typ),deps))
-  | _ -> tomatch
-
-   (* extract some ind from [t], possibly coercing from constructors in [tm] *)
-let to_mutind env isevars tm c t =
-(*  match c with
-    | Some body -> *) NotInd (c,t)
-(*    | None -> unify_tomatch_with_patterns isevars env t tm*)
-
-let type_of_tomatch = function
-  | IsInd (t,_) -> t
-  | NotInd (_,t) -> t
-
-let mkDeclTomatch na = function
-  | IsInd (t,_) -> (na,None,t)
-  | NotInd (c,t) -> (na,c,t)
-
-let map_tomatch_type f = function
-  | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
-  | NotInd (c,t) -> NotInd (Option.map f c, f t)
-
-let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
-let lift_tomatch_type n = liftn_tomatch_type n 1
-
-(**********************************************************************)
-(* Utilities on patterns *)
-
-let current_pattern eqn =
-  match eqn.patterns with
-    | pat::_ -> pat
-    | [] -> anomaly "Empty list of patterns"
-
-let alias_of_pat = function
-  | PatVar (_,name) -> name
-  | PatCstr(_,_,_,name) -> name
-
-let remove_current_pattern eqn =
-  match eqn.patterns with
-    | pat::pats ->
-	{ eqn with
-	    patterns = pats;
-	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
-    | [] -> anomaly "Empty list of patterns"
-
-let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
-
-(**********************************************************************)
-(* Well-formedness tests *)
-(* Partial check on patterns *)
-
-exception NotAdjustable
-
-let rec adjust_local_defs loc = function
-  | (pat :: pats, (_,None,_) :: decls) ->
-      pat :: adjust_local_defs loc (pats,decls)
-  | (pats, (_,Some _,_) :: decls) ->
-      PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls)
-  | [], [] -> []
-  | _ -> raise NotAdjustable
-
-let check_and_adjust_constructor env ind cstrs = function
-  | PatVar _ as pat -> pat
-  | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
-      (* Check it is constructor of the right type *)
-      let ind' = inductive_of_constructor cstr in
-      if Names.eq_ind ind' ind then
-	(* Check the constructor has the right number of args *)
-	let ci = cstrs.(i-1) in
-	let nb_args_constr = ci.cs_nargs in
-	if List.length args = nb_args_constr then pat
-	else
-	  try
-	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
-	    in PatCstr (loc, cstr, args', alias)
-	  with NotAdjustable ->
-	    error_wrong_numarg_constructor_loc loc (Global.env())
-	      cstr nb_args_constr
-      else
-	(* Try to insert a coercion *)
-	try
-	  Coercion.inh_pattern_coerce_to loc pat ind' ind
-	with Not_found ->
-	  error_bad_constructor_loc loc cstr ind
-
-let check_all_variables typ mat =
-  List.iter
-    (fun eqn -> match current_pattern eqn with
-       | PatVar (_,id) -> ()
-       | PatCstr (loc,cstr_sp,_,_) ->
-	   error_bad_pattern_loc loc cstr_sp typ)
-    mat
-
-let check_unused_pattern env eqn =
-  if not !(eqn.used) then
-    raise_pattern_matching_error
-      (eqn.eqn_loc, env, UnusedClause eqn.patterns)
-
-let set_used_pattern eqn = eqn.used := true
-
-let extract_rhs pb =
-  match pb.mat with
-    | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
-    | eqn::_ ->
-	set_used_pattern eqn;
-	eqn.rhs
-
-(**********************************************************************)
-(* Functions to deal with matrix factorization *)
-
-let occur_in_rhs na rhs =
-  match na with
-    | Anonymous -> false
-    | Name id -> occur_glob_constr id rhs.it
-
-let is_dep_patt eqn = function
-  | PatVar (_,name) -> occur_in_rhs name eqn.rhs
-  | PatCstr _ -> true
-
-let dependencies_in_rhs nargs eqns =
-  if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *)
-  else
-  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.exists ((=) true)) columns
-
-let dependent_decl a = function
-  | (na,None,t) -> dependent a t
-  | (na,Some c,t) -> dependent a t || dependent a c
-
-(* Computing the matrix of dependencies *)
-
-(* We are in context d1...dn |- and [find_dependencies k 1 nextlist]
-   computes for declaration [k+1] in which of declarations in
-   [nextlist] (which corresponds to d(k+2)...dn) it depends;
-   declarations are expressed by index, e.g. in dependency list
-   [n-2;1], [1] points to [dn] and [n-2] to [d3] *)
-
-let rec find_dependency_list k n = function
-  | [] -> []
-  | (used,tdeps,d)::rest ->
-      let deps = find_dependency_list k (n+1) rest in
-      if used && dependent_decl (mkRel n) d
-      then list_add_set (List.length rest + 1) (list_union deps tdeps)
-      else deps
-
-let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) =
-  let deps = find_dependency_list k 1 nextlist in
-  if is_dep_or_cstr_in_rhs || deps <> []
-  then (k-1,(true ,deps,d)::nextlist)
-  else (k-1,(false,[]  ,d)::nextlist)
-
-let find_dependencies_signature deps_in_rhs typs =
-  let k = List.length deps_in_rhs in
-  let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
-  List.map (fun (_,deps,_) -> deps) l
-
-(******)
-
-(* 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
-*)
-
-let regeneralize_index_tomatch n =
-  let rec genrec depth = function
-  | [] -> []
-  | Pushed ((c,tm),l)::rest ->
-      let c = regeneralize_index n depth c in
-      let tm = map_tomatch_type (regeneralize_index n depth) tm in
-      let l = List.map (regeneralize_rel n depth) l in
-      Pushed ((c,tm),l)::(genrec depth rest)
-  | Alias (c1,c2,d,t)::rest ->
-      Alias (regeneralize_index n depth c1,c2,d,t)::(genrec depth rest)
-  | Abstract d::rest ->
-      Abstract (map_rel_declaration (regeneralize_index n depth) d)
-      ::(genrec (depth+1) rest) in
-  genrec 0
-
-let rec replace_term n c k t =
-  if isRel t && destRel t = n+k then lift k c
-  else map_constr_with_binders succ (replace_term n c) k t
-
-let replace_tomatch n c =
-  let rec replrec depth = function
-  | [] -> []
-  | Pushed ((b,tm),l)::rest ->
-      let b = replace_term n c depth b in
-      let tm = map_tomatch_type (replace_term n c depth) tm in
-      List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l;
-      Pushed ((b,tm),l)::(replrec depth rest)
-  | Alias (c1,c2,d,t)::rest ->
-      Alias (replace_term n c depth c1,c2,d,t)::(replrec depth rest)
-  | Abstract d::rest ->
-      Abstract (map_rel_declaration (replace_term n c depth) d)
-      ::(replrec (depth+1) rest) in
-  replrec 0
-
-let rec liftn_tomatch_stack n depth = function
-  | [] -> []
-  | Pushed ((c,tm),l)::rest ->
-      let c = liftn n depth c in
-      let tm = liftn_tomatch_type n depth tm in
-      let l = List.map (fun i -> if i<depth then i else i+n) l in
-      Pushed ((c,tm),l)::(liftn_tomatch_stack n depth rest)
-  | Alias (c1,c2,d,t)::rest ->
-      Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t)
-      ::(liftn_tomatch_stack n depth rest)
-  | Abstract d::rest ->
-      Abstract (map_rel_declaration (liftn n depth) d)
-      ::(liftn_tomatch_stack n (depth+1) rest)
-
-
-let lift_tomatch_stack n = liftn_tomatch_stack n 1
-
-(* 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 *)
-
-(************************************************************************)
-(* Some heuristics to get names for variables pushed in pb environment *)
-(* Typical requirement:
-
-   [match y with (S (S x)) => x | x => x end] should be compiled into
-   [match y with O => y | (S n) => match n with O => y | (S x) => x end end]
-
-   and [match y with (S (S n)) => n | n => n end] into
-   [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
-
-  i.e. user names should be preserved and created names should not
-  interfere with user names *)
-
-let merge_name get_name obj = function
-  | Anonymous -> get_name obj
-  | na -> na
-
-let merge_names get_name = List.map2 (merge_name get_name)
-
-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 but
-     avoiding conflicts with user ids *)
-  let allvars =
-    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
-  let names4,_ =
-    List.fold_left2
-      (fun (l,avoid) d na ->
-	 let na =
-	   merge_name
-	     (fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid))
-	     d na
-	 in
-         (na::l,(out_name na)::avoid))
-      ([],allvars) (List.rev sign) names2 in
-  names4
-
-(************************************************************************)
-(* Recovering names for variables pushed to the rhs' environment *)
-
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
-
-let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in
-				(n, b, t)) sign
-
-let push_rels_eqn sign eqn =
-  let sign = all_name sign in
-    {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } }
-
-let push_rels_eqn_with_names sign eqn =
-  let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
-  let sign = recover_alias_names alias_of_pat pats sign in
-  push_rels_eqn sign eqn
-
-let build_aliases_context env sigma names allpats pats =
-  (* pats is the list of bodies to push as an alias *)
-  (* They all are defined in env and we turn them into a sign *)
-  (* cuts in sign need to be done in allpats *)
-  let rec insert env sign1 sign2 n newallpats oldallpats = function
-    | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) ->
-        (* Anonymous leaves must be considered named and treated in the *)
-        (* next clause because they may occur in implicit arguments *)
-	insert env sign1 sign2
-	  n newallpats (List.map List.tl oldallpats) (pats,names)
-    | (deppat,nondeppat,d,t)::pats, na::names ->
-	let nondeppat = lift n nondeppat in
-	let deppat = lift n deppat in
-	let newallpats =
-	  List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
-	let oldallpats = List.map List.tl oldallpats in
-	let decl = (na,Some deppat,t) in
-	let a = (deppat,nondeppat,d,t) in
-	insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
-	  newallpats oldallpats (pats,names)
-    | [], [] -> newallpats, sign1, sign2, env
-    | _ -> anomaly "Inconsistent alias and name lists" in
-  let allpats = List.map (fun x -> [x]) allpats
-  in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names)
-
-let insert_aliases_eqn sign eqnnames alias_rest eqn =
-  let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
-    push_rels_eqn thissign { eqn with  alias_stack = alias_rest; }
-
-
-let insert_aliases env sigma alias eqns =
-  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
-  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
-  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
-  let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
-  let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
-  (* names2 takes the meet of all needed aliases *)
-  let names2 =
-    List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in
-  (* Only needed aliases are kept by build_aliases_context *)
-  let eqnsnames, sign1, sign2, env =
-    build_aliases_context env sigma [names2] eqnsnames [alias] in
-  let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in
-  sign2, env, eqns
-
-(**********************************************************************)
-(* Functions to deal with elimination predicate *)
-
-exception Occur
-let noccur_between_without_evar n m term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel p       -> if n<=p && p<n+m then raise Occur
-    | Evar (_,cl) -> ()
-    | _             -> iter_constr_with_binders succ occur_rec n c
-  in
-  try occur_rec n term; true with Occur -> false
-
-(* Inferring the predicate *)
-let prepare_unif_pb typ cs =
-  let n = List.length (assums_of_rel_context cs.cs_args) in
-
-  (* We may need to invert ci if its parameters occur in typ *)
-  let typ' =
-    if noccur_between_without_evar 1 n typ then lift (-n) typ
-    else (* TODO4-1 *)
-      error "Unable to infer return clause of this pattern-matching problem" in
-  let args = extended_rel_list (-n) cs.cs_args in
-  let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
-
-  (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = typ' *)
-  (Array.map (lift (-n)) cs.cs_concl_realargs, ci, typ')
-
-
-(* Infering the predicate *)
-(*
-The problem to solve is the following:
-
-We match Gamma |- t : I(u01..u0q) against the following constructors:
-
-  Gamma, x11...x1p1 |- C1(x11..x1p1) : I(u11..u1q)
-   ...
-  Gamma, xn1...xnpn |- Cn(xn1..xnp1) : I(un1..unq)
-
-Assume the types in the branches are the following
-
-  Gamma, x11...x1p1 |- branch1 : T1
-   ...
-  Gamma, xn1...xnpn |- branchn : Tn
-
-Assume the type of the global case expression is Gamma |- T
-
-The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy
-the following n+1 equations:
-
-  Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1))  =  T1
-   ...
-  Gamma, xn1...xnpn |- (phi un1..unq (Cn xn1..xnpn))  =  Tn
-  Gamma             |- (phi u01..u0q t)               =  T
-
-Some hints:
-
-- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..."
-  should be inserted somewhere in Ti.
-
-- If T is undefined, an easy solution is to insert a "match z with (Ci
-  xi1..xipi) => ..." in front of each Ti
-
-- Otherwise, T1..Tn and T must be step by step unified, if some of them
-  diverge, then try to replace the diverging subterm by one of y1..yq or z.
-
-- The main problem is what to do when an existential variables is encountered
-
-let prepare_unif_pb typ cs =
-  let n = cs.cs_nargs in
-  let _,p = decompose_prod_n n typ in
-  let ci = build_dependent_constructor cs in
-  (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *)
-  (n, cs.cs_concl_realargs, ci, p)
-
-let eq_operator_lift k (n,n') = function
-  | OpRel p, OpRel p' when p > k & p' > k ->
-      if p < k+n or p' < k+n' then false else p - n = p' - n'
-  | op, op' -> op = op'
-
-let rec transpose_args n =
-  if n=0 then []
-  else
-    (Array.map (fun l -> List.hd l) lv)::
-    (transpose_args (m-1) (Array.init (fun l -> List.tl l)))
-
-let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
-
-let reloc_operator (k,n) = function OpRel p when p > k ->
-let rec unify_clauses k pv =
-  let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in
-  let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
-  if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
-  then
-    let argvl = transpose_args (List.length args1) pv' in
-    let k' = shift_operator k op1 in
-    let argl = List.map (unify_clauses k') argvl in
-    gather_constr (reloc_operator (k,n1) op1) argl
-*)
-
-let abstract_conclusion typ cs =
-  let n = List.length (assums_of_rel_context cs.cs_args) in
-  let (sign,p) = decompose_prod_n n typ in
-  it_mkLambda p sign
-
-let infer_predicate loc env isevars typs cstrs indf =
-  (* Il faudra substituer les isevars a un certain moment *)
-  if Array.length cstrs = 0 then (* "TODO4-3" *)
-    error "Inference of annotation for empty inductive types not implemented"
-  else
-    (* Empiric normalization: p may depend in a irrelevant way on args of the*)
-    (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
-    let typs =
-      Array.map (local_strong whd_beta ( !isevars)) typs
-    in
-    let eqns = array_map2 prepare_unif_pb typs cstrs in
-    (* First strategy: no dependencies at all *)
-(*
-    let (mis,_) = dest_ind_family indf in
-    let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
-*)
-    let (sign,_) = get_arity env indf in
-    let mtyp =
-      if array_exists is_Type typs then
-	(* Heuristic to avoid comparison between non-variables algebric univs*)
-	new_Type ()
-      else
-	mkExistential env ~src:(loc, Evd.CasesType) isevars
-    in
-    if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
-    then
-      (* Non dependent case -> turn it into a (dummy) dependent one *)
-      let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
-      let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
-      (true,pred) (* true = dependent -- par défaut *)
-    else
-(*
-      let s = get_sort_of env ( isevars) typs.(0) in
-      let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
-      let caseinfo = make_default_case_info mis in
-      let brs = array_map2 abstract_conclusion typs cstrs in
-      let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
-      let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
-*)
-      (* "TODO4-2" *)
-      (* We skip parameters *)
-      let cis =
-	Array.map
-	  (fun cs ->
-	     applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args))
-	  cstrs in
-      let ct = array_map2 (fun ci (_,_,t) -> (ci,t)) cis eqns in
-      raise_pattern_matching_error (loc,env, CannotInferPredicate ct)
-(*
-      (true,pred)
-*)
-
-(* Propagation of user-provided predicate through compilation steps *)
-
-let rec map_predicate f k = function
-  | PrCcl ccl -> PrCcl (f k ccl)
-  | PrProd pred ->
-      PrProd (map_predicate f (k+1) pred)
-  | PrLetIn ((names,dep as tm),pred) ->
-      let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
-      PrLetIn (tm, map_predicate f (k+k') pred)
-
-let rec noccurn_predicate k = function
-  | PrCcl ccl -> noccurn k ccl
-  | PrProd pred -> noccurn_predicate (k+1) pred
-  | PrLetIn ((names,dep),pred) ->
-      let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
-      noccurn_predicate (k+k') pred
-
-let liftn_predicate n = map_predicate (liftn n)
-
-let lift_predicate n = liftn_predicate n 1
-
-let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0
-
-let substnl_predicate sigma = map_predicate (substnl sigma)
-
-(* This is parallel bindings *)
-let subst_predicate (args,copt) pred =
-  let sigma = match copt with
-    | None -> List.rev args
-    | Some c -> c::(List.rev args) in
-  substnl_predicate sigma 0 pred
-
-let specialize_predicate_var (cur,typ) = function
-  | PrProd _ | PrCcl _ ->
-     anomaly "specialize_predicate_var: a pattern-variable must be pushed"
-  | PrLetIn (([],dep),pred) ->
-      subst_predicate ([],if dep<>Anonymous then Some cur else None) pred
-  | PrLetIn ((_,dep),pred) ->
-      (match typ with
-        | IsInd (_,IndType (_,realargs)) ->
-           subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred
-        | _ -> anomaly "specialize_predicate_var")
-
-let ungeneralize_predicate = function
-  | PrLetIn _ | PrCcl _ -> anomaly "ungeneralize_predicate: expects a product"
-  | PrProd pred -> pred
-
-(*****************************************************************************)
-(* We have pred = [X:=realargs;x:=c]P typed in Gamma1, x:I(realargs), Gamma2 *)
-(* and we want to abstract P over y:t(x) typed in the same context to get    *)
-(*                                                                           *)
-(*    pred' = [X:=realargs;x':=c](y':t(x'))P[y:=y']                          *)
-(*                                                                           *)
-(* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x'        *)
-(* then we have to replace x by x' in t(x) and y by y' in P                  *)
-(*****************************************************************************)
-let generalize_predicate ny d = function
-  | PrLetIn ((names,dep as tm),pred) ->
-      if dep=Anonymous then anomaly "Undetected dependency";
-      let p = List.length names + 1 in
-      let pred = lift_predicate 1 pred in
-      let pred = regeneralize_index_predicate (ny+p+1) pred in
-      PrLetIn (tm, PrProd pred)
-  | PrProd _ | PrCcl _ ->
-      anomaly "generalize_predicate: expects a non trivial pattern"
-
-let rec extract_predicate l = function
-  | pred, Alias (deppat,nondeppat,_,_)::tms ->
-      let tms' = match kind_of_term nondeppat with
-        | Rel i -> replace_tomatch i deppat tms
-        | _ -> (* initial terms are not dependent *) tms in
-      extract_predicate l (pred,tms')
-  | PrProd pred, Abstract d'::tms ->
-      let d' = map_rel_declaration (lift (List.length l)) d' in
-      substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms)))
-  | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms ->
-      extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
-  | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms ->
-      let l = List.rev realargs@l in
-      extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
-  | PrCcl ccl, [] ->
-      substl l ccl
-  | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match"
-
-let abstract_predicate env sigma indf cur tms = function
-  | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn"
-  | PrLetIn ((names,dep),pred) ->
-      let sign = make_arity_signature env true indf in
-      (* n is the number of real args + 1 *)
-      let n = List.length sign in
-      let tms = lift_tomatch_stack n tms in
-      let tms =
-        match kind_of_term cur with
-          | Rel i -> regeneralize_index_tomatch (i+n) tms
-          | _ -> (* Initial case *) tms in
-      (* Depending on whether the predicate is dependent or not, and has real
-         args or not, we lift it to make room for [sign] *)
-      (* Even if not intrinsically dep, we move the predicate into a dep one *)
-      let sign,k =
-        if names = [] & n <> 1 then
-          (* Real args were not considered *)
-          (if dep<>Anonymous then
-            ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
-          else
-            (sign,n))
-        else
-          (* Real args are OK *)
-          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
-           if dep<>Anonymous then 0 else 1) in
-      let pred = lift_predicate k pred in
-      let pred = extract_predicate [] (pred,tms) in
-      (true, it_mkLambda_or_LetIn_name env pred sign)
-
-let rec known_dependent = function
-  | None -> false
-  | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous
-  | Some (PrCcl _) -> false
-  | Some (PrProd _) ->
-      anomaly "known_dependent: can only be used when patterns remain"
-
-(* [expand_arg] is used by [specialize_predicate]
-   it replaces gamma, x1...xn, x1...xk |- pred
-   by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or
-   by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *)
-
-let expand_arg n alreadydep (na,t) deps (k,pred) =
-  (* current can occur in pred even if the original problem is not dependent *)
-  let dep =
-    if alreadydep<>Anonymous then alreadydep
-    else if deps = [] && noccurn_predicate 1 pred then Anonymous
-    else Name (id_of_string "x") in
-  let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in
-  (* There is no dependency in realargs for subpattern *)
-  (k-1, PrLetIn (([],dep), pred))
-
-
-(*****************************************************************************)
-(* pred = [X:=realargs;x:=c]P types the following problem:                   *)
-(*                                                                           *)
-(*  Gamma |- match Pushed(c:I(realargs)) rest with...end: pred               *)
-(*                                                                           *)
-(* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi)      *)
-(* is considered. Assume each Ti is some Ii(argsi).                          *)
-(* We let e=Ci(x1,...,xn) and replace pred by                                *)
-(*                                                                           *)
-(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *)
-(*                                                                           *)
-(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
-(*                                                                           *)
-(*****************************************************************************)
-let specialize_predicate tomatchs deps cs = function
-  | (PrProd _ | PrCcl _) ->
-      anomaly "specialize_predicate: a matched pattern must be pushed"
-  | PrLetIn ((names,isdep),pred) ->
-      (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *)
-      let nrealargs = List.length names in
-      let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in
-      (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *)
-      let n = cs.cs_nargs in
-      let pred' = liftn_predicate n (k+1) pred in
-      let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
-      let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in
-      (* The substituends argsi, copti are all defined in gamma, x1...xn *)
-      (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *)
-      let pred'' = subst_predicate (argsi, copti) pred' in
-      (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *)
-      let pred''' = liftn_predicate n (n+1) pred'' in
-      (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
-      snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred'''))
-
-let find_predicate loc env isevars p typs cstrs current
-  (IndType (indf,realargs)) tms =
-  let (dep,pred) =
-    match p with
-      | Some p -> abstract_predicate env ( !isevars) indf current tms p
-      | None -> infer_predicate loc env isevars typs cstrs indf in
-  let typ = whd_beta ( !isevars) (applist (pred, realargs)) in
-  if dep then
-    (pred, whd_beta ( !isevars) (applist (typ, [current])),
-     new_Type ())
-  else
-    (pred, typ, new_Type ())
-
-(************************************************************************)
-(* Sorting equations by constructor *)
-
-type inversion_problem =
-  (* the discriminating arg in some Ind and its order in Ind *)
-  | Incompatible of int * (int * int)
-  | Constraints of (int * constr) list
-
-let solve_constraints constr_info indt =
-  (* TODO *)
-  Constraints []
-
-let rec irrefutable env = function
-  | PatVar (_,name) -> true
-  | PatCstr (_,cstr,args,_) ->
-      let ind = inductive_of_constructor cstr in
-      let (_,mip) = Inductive.lookup_mind_specif env ind in
-      let one_constr = Array.length mip.mind_user_lc = 1 in
-      one_constr & List.for_all (irrefutable env) args
-
-let first_clause_irrefutable env = function
-  | eqn::mat -> List.for_all (irrefutable env) eqn.patterns
-  | _ -> false
-
-let group_equations pb ind current cstrs mat =
-  let mat =
-    if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
-  let brs = Array.create (Array.length cstrs) [] in
-  let only_default = ref true in
-  let _ =
-    List.fold_right (* To be sure it's from bottom to top *)
-      (fun eqn () ->
-	 let rest = remove_current_pattern eqn in
-	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor pb.env ind cstrs pat with
-	   | PatVar (_,name) ->
-	       (* This is a default clause that we expand *)
-	       for i=1 to Array.length cstrs do
-		 let n = cstrs.(i-1).cs_nargs in
-		 let args = make_anonymous_patvars n in
-		 brs.(i-1) <- (args, rest) :: brs.(i-1)
-	       done
-	   | PatCstr (loc,((_,i)),args,_) ->
-	       (* This is a regular clause *)
-	       only_default := false;
-	       brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
-  (brs,!only_default)
-
-(************************************************************************)
-(* Here starts the pattern-matching compilation algorithm *)
-
-(* Abstracting over dependent subterms to match *)
-let rec generalize_problem pb = function
-  | [] -> pb
-  | i::l ->
-      let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
-      let pb' = generalize_problem pb l in
-      let tomatch = lift_tomatch_stack 1 pb'.tomatch in
-      let tomatch = regeneralize_index_tomatch (i+1) tomatch in
-      { pb with
-	  tomatch = Abstract d :: tomatch;
-          pred = Option.map (generalize_predicate i d) pb'.pred }
-
-(* No more patterns: typing the right-hand side of equations *)
-let build_leaf pb =
-  let rhs = extract_rhs pb in
-  let tycon = match pb.pred with
-    | None -> anomaly "Predicate not found"
-    | Some (PrCcl typ) -> mk_tycon typ
-    | Some _ -> anomaly "not all parameters of pred have been consumed" in
-    pb.typing_function tycon rhs.rhs_env rhs.it
-
-(* Building the sub-problem when all patterns are variables *)
-let shift_problem (current,t) pb =
-  {pb with
-     tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
-     history = push_history_pattern 0 AliasLeaf pb.history;
-     mat = List.map remove_current_pattern pb.mat }
-
-(* Building the sub-pattern-matching problem for a given branch *)
-let build_branch current deps pb eqns const_info =
-  (* We remember that we descend through a constructor *)
-  let alias_type =
-    if Array.length const_info.cs_concl_realargs = 0
-      & not (known_dependent pb.pred) & deps = []
-    then
-      NonDepAlias
-    else
-      DepAlias
-  in
-  let history =
-    push_history_pattern const_info.cs_nargs
-      (AliasConstructor const_info.cs_cstr)
-      pb.history in
-
-  (* We find matching clauses *)
-  let cs_args = (*assums_of_rel_context*) const_info.cs_args in
-  let names = get_names pb.env cs_args eqns in
-  let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
-  if submat = [] then
-    raise_pattern_matching_error
-      (dummy_loc, pb.env, NonExhaustive (complete_history history));
-  let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in
-  let _,typs',_ =
-    List.fold_right
-      (fun (na,c,t as d) (env,typs,tms) ->
-	 let tm1 = List.map List.hd tms in
-	 let tms = List.map List.tl tms in
- 	 (push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms))
-      typs (pb.env,[],List.map fst eqns) in
-
-  let dep_sign =
-    find_dependencies_signature
-      (dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in
-
-  (* The dependent term to subst in the types of the remaining UnPushed
-     terms is relative to the current context enriched by topushs *)
-  let ci = build_dependent_constructor const_info in
-
-  (* We replace [(mkRel 1)] by its expansion [ci] *)
-  (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *)
-  (* This is done in two steps : first from "Gamma |- tms" *)
-  (* into  "Gamma; typs; curalias |- tms" *)
-  let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
-
-  let currents =
-    list_map2_i
-      (fun i (na,t) deps -> Pushed ((mkRel i, lift_tomatch_type i t), deps))
-      1 typs' (List.rev dep_sign) in
-
-  let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in
-  let ind =
-    appvect (
-      applist (mkInd (inductive_of_constructor const_info.cs_cstr),
-      List.map (lift const_info.cs_nargs) const_info.cs_params),
-      const_info.cs_concl_realargs) in
-
-  let cur_alias = lift (List.length sign) current in
-  let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
-  let env' = push_rels sign pb.env in
-  let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
-    sign,
-  { pb with
-      env = env';
-      tomatch = List.rev_append currents tomatch;
-      pred = pred';
-      history = history;
-      mat = List.map (push_rels_eqn_with_names sign) submat }
-
-(**********************************************************************
- INVARIANT:
-
-  pb = { env, subst, tomatch, mat, ...}
-  tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T)
-
-  "Pushed" terms and types are relative to env
-  "Abstract" types are relative to env enriched by the previous terms to match
-
-*)
-
-(**********************************************************************)
-(* Main compiling descent *)
-let rec compile pb =
-  match pb.tomatch with
-    | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur
-    | (Alias x)::rest -> compile_alias pb x rest
-    | (Abstract d)::rest -> compile_generalization pb d rest
-    | [] -> build_leaf pb
-
-and match_current pb tomatch =
-  let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in
-  match typ with
-    | NotInd (_,typ) ->
-	check_all_variables typ pb.mat;
-	compile (shift_problem ct pb)
-    | IsInd (_,(IndType(indf,realargs) as indt)) ->
-	let mind,_ = dest_ind_family indf in
-	let cstrs = get_constructors pb.env indf in
-	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
-	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
-	  compile (shift_problem ct pb)
-	else
-          let _constraints = Array.map (solve_constraints indt) cstrs in
-
-	  (* We generalize over terms depending on current term to match *)
-	  let pb = generalize_problem pb deps in
-
-	  (* We compile branches *)
-	  let brs = array_map2 (compile_branch current deps pb) eqns cstrs in
-
-	  (* We build the (elementary) case analysis *)
-	  let brvals = Array.map (fun (v,_) -> v) brs in
-	  let brtyps = Array.map (fun (_,t) -> t) brs in
-	  let (pred,typ,s) =
-	    find_predicate pb.caseloc pb.env pb.isevars
-	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
-	  let inst = List.map mkRel deps in
-	  { uj_val = applist (case, inst);
-	    uj_type = substl inst typ }
-
-and compile_branch current deps pb eqn cstr =
-  let sign, pb = build_branch current deps pb eqn cstr in
-  let j = compile pb in
-  (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
-
-and compile_generalization pb d rest =
-  let pb =
-    { pb with
-       env = push_rel d pb.env;
-       tomatch = rest;
-       pred = Option.map ungeneralize_predicate pb.pred;
-       mat = List.map (push_rels_eqn [d]) pb.mat } in
-  let j = compile pb in
-  { uj_val = mkLambda_or_LetIn d j.uj_val;
-    uj_type = mkProd_or_LetIn d j.uj_type }
-
-and compile_alias pb (deppat,nondeppat,d,t) rest =
-  let history = simplify_history pb.history in
-  let sign, newenv, mat =
-    insert_aliases pb.env ( !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
-  let n = List.length sign in
-
-  (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
-  (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *)
-  let tomatch = lift_tomatch_stack n rest in
-  let tomatch = match kind_of_term nondeppat with
-    | Rel i ->
-	if n = 1 then regeneralize_index_tomatch (i+n) tomatch
-	else replace_tomatch i deppat tomatch
-    | _ -> (* initial terms are not dependent *) tomatch in
-
-  let pb =
-    {pb with
-       env = newenv;
-       tomatch = tomatch;
-       pred = Option.map (lift_predicate n) pb.pred;
-       history = history;
-       mat = mat } in
-  let j = compile pb in
-  List.fold_left mkSpecialLetInJudge j sign
-
-(* 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 eqn has n patterns
- * and linearizing the _ patterns.
- * Syntactic correctness has already been done in astterm *)
-let matx_of_eqns env eqns =
-  let build_eqn (loc,ids,lpat,rhs) =
-    let rhs =
-      { rhs_env = env;
-	avoid_ids = ids@(ids_of_named_context (named_context env));
-	it = rhs;
-      } in
-    { patterns = lpat;
-      alias_stack = [];
-      eqn_loc = loc;
-      used = ref false;
-      rhs = rhs }
-  in List.map build_eqn eqns
-
-(************************************************************************)
-(* preparing the elimination predicate if any                          *)
-
-let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
-  let cook (n, l, env, signs) = function
-    | c,IsInd (_,IndType(indf,realargs)) ->
-	let indf' = lift_inductive_family n indf in
-	let sign = make_arity_signature env dep indf' in
-	let p = List.length realargs in
-	if dep then
-	  (n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs)
-	else
-	  (n + p, (List.rev realargs)@l, push_rels sign env,sign::signs)
-    | c,NotInd _ ->
-	(n, l, env, []::signs) in
-  let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in
-  let names = List.rev (List.map (List.map pi1) signs) in
-  let allargs =
-    List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in
-  let rec build_skeleton env c =
-    (* Don't put into normal form, it has effects on the synthesis of evars *)
- (* let c = whd_betadeltaiota env ( isevars) c in *)
-    (* We turn all subterms possibly dependent into an evar with maximum ctxt*)
-    if isEvar c or List.exists (eq_constr c) allargs then
-      e_new_evar isevars env  ~src:(loc, Evd.CasesType)
-        (Retyping.get_type_of env ( !isevars) c)
-    else
-      map_constr_with_full_binders push_rel build_skeleton env c
-  in
-    names, build_skeleton env (lift n c)
-
-(* Here, [pred] is assumed to be in the context built from all *)
-(* realargs and terms to match *)
-let build_initial_predicate isdep allnames pred =
-  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
-  let rec buildrec n pred = function
-    | [] -> PrCcl pred
-    | names::lnames ->
-        let names' = if isdep then List.tl names else names in
-        let n' = n + List.length names' in
-        let pred, p, user_p =
-          if isdep then
-            if dependent (mkRel (nar-n')) pred then pred, 1, 1
-            else liftn (-1) (nar-n') pred, 0, 1
-          else pred, 0, 0 in
-        let na =
-          if p=1 then
-            let na = List.hd names in
-            if na = Anonymous then
-              (* peut arriver en raison des evars *)
-              Name (id_of_string "x") (*Hum*)
-            else na
-          else Anonymous in
-        PrLetIn ((names',na), buildrec (n'+user_p) pred lnames)
-  in buildrec 0 pred allnames
-
-let extract_arity_signature env0 tomatchl tmsign =
-  let get_one_sign n tm (na,t) =
-    match tm with
-      | NotInd (bo,typ) ->
-	  (match t with
-	    | None -> [na,Option.map (lift n) bo,lift n typ]
-	    | Some (loc,_,_) ->
- 	    user_err_loc (loc,"",
-	    str "Unexpected type annotation for a term of non inductive type"))
-      | IsInd (_,IndType(indf,realargs)) ->
-          let indf' = lift_inductive_family n indf in
-	  let (ind,params) = dest_ind_family indf' in
-	  let nrealargs = List.length realargs in
-	  let realnal =
-	    match t with
-	      | Some (loc,ind',realnal) ->
-		  if ind <> ind' then
-		    user_err_loc (loc,"",str "Wrong inductive type");
-		  if nrealargs <> List.length realnal then
-		      anomaly "Ill-formed 'in' clause in cases";
-		  List.rev realnal
-	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
-	  let arsign = fst (get_arity env0 indf') in
-	  (na,None,build_dependent_inductive env0 indf')
-	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
-  let rec buildrec n = function
-    | [],[] -> []
-    | (_,tm)::ltm, x::tmsign ->
-	let l = get_one_sign n tm x in
-	l :: buildrec (n + List.length l) (ltm,tmsign)
-    | _ -> assert false
-  in List.rev (buildrec 0 (tomatchl,tmsign))
-
-let extract_arity_signatures env0 tomatchl tmsign =
-  let get_one_sign tm (na,t) =
-    match tm with
-      | NotInd (bo,typ) ->
-	  (match t with
-	    | None -> [na,bo,typ]
-	    | Some (loc,_,_) ->
- 	    user_err_loc (loc,"",
-	    str "Unexpected type annotation for a term of non inductive type"))
-      | IsInd (_,IndType(indf,realargs)) ->
-	  let (ind,params) = dest_ind_family indf in
-	  let nrealargs = List.length realargs in
-	  let realnal =
-	    match t with
-	      | Some (loc,ind',realnal) ->
-		  if ind <> ind' then
-		    user_err_loc (loc,"",str "Wrong inductive type");
-		  if nrealargs <> List.length realnal then
-		      anomaly "Ill-formed 'in' clause in cases";
-		  List.rev realnal
-	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
-	  let arsign = fst (get_arity env0 indf) in
-	    (na,None,build_dependent_inductive env0 indf)
-	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
-  let rec buildrec = function
-    | [],[] -> []
-    | (_,tm)::ltm, x::tmsign ->
-	let l = get_one_sign tm x in
-	  l :: buildrec (ltm,tmsign)
-    | _ -> assert false
-  in List.rev (buildrec (tomatchl,tmsign))
-
-let inh_conv_coerce_to_tycon loc env isevars j tycon =
-  match tycon with
-    | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
-          isevars := evd';
-          j
-    | None -> j
-
-let string_of_name name =
-  match name with
-    | Anonymous -> "anonymous"
-    | Name n -> string_of_id n
-
-let id_of_name n = id_of_string (string_of_name n)
-
-let make_prime_id name =
-  let str = string_of_name name in
-    id_of_string str, id_of_string (str ^ "'")
-
-let prime avoid name =
-  let previd, id = make_prime_id name in
-    previd, next_ident_away id avoid
-
-let make_prime avoid prevname =
-  let previd, id = prime !avoid prevname in
-    avoid := id :: !avoid;
-    previd, id
-
-let eq_id avoid id =
-  let hid = id_of_string ("Heq_" ^ string_of_id id) in
-  let hid' = next_ident_away hid avoid in
-    hid'
-
-let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y =
-  mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
-
-let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
-
-let constr_of_pat env isevars arsign pat avoid =
-  let rec typ env (ty, realargs) pat avoid =
-    match pat with
-    | PatVar (l,name) ->
-	let name, avoid = match name with
-	    Name n -> name, avoid
-	  | Anonymous ->
-	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
-		Name id, id :: avoid
-	in
-	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
-    | PatCstr (l,((_, i) as cstr),args,alias) ->
-	let cind = inductive_of_constructor cstr in
-	let IndType (indf, _) = 
-	  try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
-	  with Not_found -> error_case_not_inductive env 
-	    {uj_val = ty; uj_type = Typing.type_of env !isevars ty}
-	in
-	let ind, params = dest_ind_family indf in
-	if ind <> cind then error_bad_constructor_loc l cstr ind;
-	let cstrs = get_constructors env indf in
-	let ci = cstrs.(i-1) in
-	let nb_args_constr = ci.cs_nargs in
-	assert(nb_args_constr = List.length args);
-	let patargs, args, sign, env, n, m, avoid =
-	  List.fold_right2
-	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid)  ->
-	       let pat', sign', arg', typ', argtypargs, n', avoid =
-		 typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid
-	       in
-	       let args' = arg' :: List.map (lift n') args in
-	       let env' = push_rels sign' env in
-		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
-	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
-	in
-	let args = List.rev args in
-	let patargs = List.rev patargs in
-	let pat' = PatCstr (l, cstr, patargs, alias) in
-	let cstr = mkConstruct ci.cs_cstr in
-	let app = applistc cstr (List.map (lift (List.length sign)) params) in
-	let app = applistc app args in
-	let apptype = Retyping.get_type_of env ( !isevars) app in
-	let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
-	  match alias with
-	      Anonymous ->
-		pat', sign, app, apptype, realargs, n, avoid
-	    | Name id ->
-		let sign = (alias, None, lift m ty) :: sign in
-		let avoid = id :: avoid in
-		let sign, i, avoid =
-		  try
-		    let env = push_rels sign env in
-		    isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars;
-		    let eq_t = mk_eq (lift (succ m) ty)
-		      (mkRel 1) (* alias *)
-		      (lift 1 app) (* aliased term *)
-		    in
-		    let neq = eq_id avoid id in
-		      (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
-		  with Reduction.NotConvertible -> sign, 1, avoid
-		in
-		  (* Mark the equality as a hole *)
-		  pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
-  in
-  let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in
-    pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid
-
-
-(* shadows functional version *)
-let eq_id avoid id =
-  let hid = id_of_string ("Heq_" ^ string_of_id id) in
-  let hid' = next_ident_away hid !avoid in
-    avoid := hid' :: !avoid;
-    hid'
-
-let rels_of_patsign =
-  List.map (fun ((na, b, t) as x) ->
-    match b with
-      | Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
-      | _ -> x)
-
-let vars_of_ctx ctx =
-  let _, y =
-    List.fold_right (fun (na, b, t)  (prev, vars) ->
-      match b with
-	| Some t' when kind_of_term t' = Rel 0 ->
-	    prev,
-	    (GApp (dummy_loc,
-		(GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars
-	| _ ->
-	    match na with
-		Anonymous -> raise (Invalid_argument "vars_of_ctx")
-	      | Name n -> n, GVar (dummy_loc, n) :: vars)
-      ctx (id_of_string "vars_of_ctx_error", [])
-  in List.rev y
-
-let rec is_included x y =
-  match x, y with
-    | PatVar _, _ -> true
-    | _, PatVar _ -> true
-    | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias')  ->
-	if i = i' then List.for_all2 is_included args args'
-	else false
-
-(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its
-   full signature. However prevpatterns are in the original one signature per pattern form.
- *)
-let build_ineqs prevpatterns pats liftsign =
-  let _tomatchs = List.length pats in
-  let diffs =
-    List.fold_left
-      (fun c eqnpats ->
-	  let acc = List.fold_left2
-	    (* ppat is the pattern we are discriminating against, curpat is the current one. *)
-	    (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat)
-	      (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
-	      match acc with
-		  None -> None
-		| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
-		    if is_included curpat ppat then
-		      (* Length of previous pattern's signature *)
-		      let lens = List.length ppat_sign in
-		      (* Accumulated length of previous pattern's signatures *)
-		      let len' = lens + len in
-		      let acc =
-			((* Jump over previous prevpat signs *)
-			  lift_rel_context len ppat_sign @ sign,
-			  len',
-			  succ n, (* nth pattern *)
-			  mkApp (delayed_force eq_ind,
-				[| lift (len' + liftsign) curpat_ty;
-				   liftn (len + liftsign) (succ lens) ppat_c ;
-				   lift len' curpat_c |]) ::
-			    List.map (lift lens (* Jump over this prevpat signature *)) c)
-		      in Some acc
-		    else None)
-	   (Some ([], 0, 0, [])) eqnpats pats
-	 in match acc with
-	     None -> c
-	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_not (mk_conj c'))
-		 (lift_rel_context liftsign sign)
-	       in
-		 conj :: c)
-      [] prevpatterns
-  in match diffs with [] -> None
-    | _ -> Some (mk_conj diffs)
-
-let subst_rel_context k ctx subst =
-  let (_, ctx') =
-    List.fold_right
-      (fun (n, b, t) (k, acc) ->
-	 (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
-      ctx (k, [])
-  in ctx'
-
-let lift_rel_contextn n k sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
-    | [] -> []
-  in
-  liftrec (rel_context_length sign + k) sign
-
-let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
-  let i = ref 0 in
-  let (x, y, z) =
-    List.fold_left
-      (fun (branches, eqns, prevpatterns) eqn ->
-	 let _, newpatterns, pats =
-	   List.fold_left2
-	     (fun (idents, newpatterns, pats) pat arsign ->
-		let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
-		  (idents, pat' :: newpatterns, cpat :: pats))
-	      ([], [], []) eqn.patterns sign
-	 in
-	 let newpatterns = List.rev newpatterns and opats = List.rev pats in
-	 let rhs_rels, pats, signlen =
-	   List.fold_left
-	     (fun (renv, pats, n) (sign,c, (s, args), p) ->
-	       (* Recombine signatures and terms of all of the row's patterns *)
-	       let sign' = lift_rel_context n sign in
-	       let len = List.length sign' in
-		 (sign' @ renv,
-		 (* lift to get outside of previous pattern's signatures. *)
-		 (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
-		 len + n))
-	     ([], [], 0) opats in
-	 let pats, _ = List.fold_left
-	   (* lift to get outside of past patterns to get terms in the combined environment. *)
-	   (fun (pats, n) (sign, c, (s, args), p) ->
-	     let len = List.length sign in
-	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
-	   ([], 0) pats
-	 in
-	 let ineqs = build_ineqs prevpatterns pats signlen in
-	 let rhs_rels' = rels_of_patsign rhs_rels in
-	 let _signenv = push_rel_context rhs_rels' env in
-	 let arity =
-	   let args, nargs =
-	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
-	       (args @ c :: allargs, List.length args + succ n))
-	       pats ([], 0)
-	   in
-	   let args = List.rev args in
-	     substl args (liftn signlen (succ nargs) arity)
-	 in
-	 let rhs_rels', tycon =
-	   let neqs_rels, arity =
-	     match ineqs with
-	     | None -> [], arity
-	     | Some ineqs ->
-		 [Anonymous, None, ineqs], lift 1 arity
-	   in
-	   let eqs_rels, arity = decompose_prod_n_assum neqs arity in
-	     eqs_rels @ neqs_rels @ rhs_rels', arity
-	 in
-	 let rhs_env = push_rels rhs_rels' env in
-	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
-	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
-	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
-	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
-	 let branch =
-	   let bref = GVar (dummy_loc, branch_name) in
-	     match vars_of_ctx rhs_rels with
-		 [] -> bref
-	       | l -> GApp (dummy_loc, bref, l)
-	 in
-	 let branch = match ineqs with
-	     Some _ -> GApp (dummy_loc, branch, [ hole ])
-	   | None -> branch
-	 in
-	 incr i;
-	 let rhs = { eqn.rhs with it = branch } in
-	   (branch_decl :: branches,
-	   { eqn with patterns = newpatterns; rhs = rhs } :: eqns,
-	   opats :: prevpatterns))
-      ([], [], []) eqns
-  in x, y
-
-(* Builds the predicate. If the predicate is dependent, its context is
- * made of 1+nrealargs assumptions for each matched term in an inductive
- * type and 1 assumption for each term not _syntactically_ in an
- * inductive type.
-
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: it is assumed non dependent.
- *)
-
-let lift_ctx n ctx =
-  let ctx', _ =
-    List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
-  in ctx'
-
-(* Turn matched terms into variables. *)
-let abstract_tomatch env tomatchs tycon =
-  let prev, ctx, names, tycon =
-    List.fold_left
-      (fun (prev, ctx, names, tycon) (c, t) ->
-	 let lenctx =  List.length ctx in
-	 match kind_of_term c with
-	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
-	   | _ ->
-	       let tycon = Option.map
-		 (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
-	       let name = next_ident_away (id_of_string "filtered_var") names in
-		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
-	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
-	       name :: names, tycon)
-      ([], [], [], tycon) tomatchs
-  in List.rev prev, ctx, tycon
-
-let is_dependent_ind = function
-    IsInd (_, IndType (indf, args)) when List.length args > 0 -> true
-  | _ -> false
-
-let build_dependent_signature env evars avoid tomatchs arsign =
-  let avoid = ref avoid in
-  let arsign = List.rev arsign in
-  let allnames = List.rev (List.map (List.map pi1) arsign) in
-  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
-  let eqs, neqs, refls, slift, arsign' =
-    List.fold_left2
-      (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign ->
-	 (* The accumulator:
-	    previous eqs,
-	    number of previous eqs,
-	    lift to get outside eqs and in the introduced variables ('as' and 'in'),
-	    new arity signatures
-	 *)
-	 match ty with
-	     IsInd (ty, IndType (indf, args)) when List.length args > 0 ->
-	       (* Build the arity signature following the names in matched terms as much as possible *)
-	       let argsign = List.tl arsign in (* arguments in inverse application order *)
-	       let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
-	       let argsign = List.rev argsign in (* arguments in application order *)
-	       let env', nargeqs, argeqs, refl_args, slift, argsign' =
-		 List.fold_left2
-		   (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
-		      let argt = Retyping.get_type_of env evars arg in
-		      let eq, refl_arg =
-			if Reductionops.is_conv env evars argt t then
-			  (mk_eq (lift (nargeqs + slift) argt)
-			     (mkRel (nargeqs + slift))
-			     (lift (nargeqs + nar) arg),
-			   mk_eq_refl argt arg)
-			else
-			  (mk_JMeq (lift (nargeqs + slift) t)
-			     (mkRel (nargeqs + slift))
-			     (lift (nargeqs + nar) argt)
-			     (lift (nargeqs + nar) arg),
-			   mk_JMeq_refl argt arg)
-		      in
-		      let previd, id =
-			let name =
-			  match kind_of_term arg with
-			      Rel n -> pi1 (lookup_rel n env)
-			    | _ -> name
-			in
-			  make_prime avoid name
-		      in
-			(env, succ nargeqs,
-			 (Name (eq_id avoid previd), None, eq) :: argeqs,
-			 refl_arg :: refl_args,
-			 pred slift,
-			 (Name id, b, t) :: argsign'))
-		   (env, neqs, [], [], slift, []) args argsign
-	       in
-	       let eq = mk_JMeq
-		 (lift (nargeqs + slift) appt)
-		 (mkRel (nargeqs + slift))
-		 (lift (nargeqs + nar) ty)
-		 (lift (nargeqs + nar) tm)
-	       in
-	       let refl_eq = mk_JMeq_refl ty tm in
-	       let previd, id = make_prime avoid appn in
-		 (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
-		 succ nargeqs,
-		 refl_eq :: refl_args,
-		 pred slift,
-		 (((Name id, appb, appt) :: argsign') :: arsigns))
-
-	   | _ ->
-	       (* Non dependent inductive or not inductive, just use a regular equality *)
-	       let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
-	       let previd, id = make_prime avoid name in
-	       let arsign' = (Name id, b, typ) in
-	       let tomatch_ty = type_of_tomatch ty in
-	       let eq =
-		 mk_eq (lift nar tomatch_ty)
-		   (mkRel slift) (lift nar tm)
-	       in
-		 ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
-		  (mk_eq_refl tomatch_ty tm) :: refl_args,
-		  pred slift, (arsign' :: []) :: arsigns))
-      ([], 0, [], nar, []) tomatchs arsign
-  in
-  let arsign'' = List.rev arsign' in
-    assert(slift = 0); (* we must have folded over all elements of the arity signature *)
-    arsign'', allnames, nar, eqs, neqs, refls
-
-(**************************************************************************)
-(* Main entry of the matching compilation                                 *)
-
-let liftn_rel_context n k sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
-    | [] -> []
-  in
-    liftrec (k + rel_context_length sign) sign
-
-let nf_evars_env sigma (env : env) : env =
-  let nf t = nf_evar sigma t in
-  let env0 : env = reset_context env in
-  let f e (na, b, t) e' : env =
-    Environ.push_named (na, Option.map nf b, nf t) e'
-  in
-  let env' = Environ.fold_named_context f ~init:env0 env in
-    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
-     ~init:env' env
-
-
-let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
-  (* We extract the signature of the arity *)
-  let arsign = extract_arity_signature env tomatchs sign in
-  let newenv = List.fold_right push_rels arsign env in
-  let allnames = List.rev (List.map (List.map pi1) arsign) in
-    match rtntyp with
-      | Some rtntyp ->
-	  let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
-	  let predccl = (j_nf_evar !isevars predcclj).uj_val in
-	    Some (build_initial_predicate true allnames predccl)
-      | None ->
-	  match valcon_of_tycon tycon with
-	    | Some ty ->
-		let pred =
-		  prepare_predicate_from_arsign_tycon loc env !isevars tomatchs arsign ty
-		in Some (build_initial_predicate true allnames pred)
-	    | None -> None
-
-let compile_program_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
-
-  let typing_fun tycon env = typing_fun tycon env isevars in
-
-  (* 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
-  let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in
-    if predopt = None then
-      let tycon = valcon_of_tycon tycon in
-      let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in
-      let env = push_rel_context tomatchs_lets env in
-      let len = List.length eqns in
-      let sign, allnames, signlen, eqs, neqs, args =
-	(* The arity signature *)
-	let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in
-	  (* Build the dependent arity signature, the equalities which makes
-	     the first part of the predicate and their instantiations. *)
-	let avoid = [] in
-	  build_dependent_signature env ( !isevars) avoid tomatchs arsign
-
-      in
-      let tycon, arity =
-	match tycon' with
-	| None -> let ev = mkExistential env isevars in ev, ev
-	| Some t ->
-	    Option.get tycon, prepare_predicate_from_arsign_tycon loc env ( !isevars)
-	      tomatchs sign t
-      in
-      let neqs, arity =
-	let ctx = context_of_arsign eqs in
-	let neqs = List.length ctx in
-	  neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
-      in
-      let lets, matx =
-	(* Type the rhs under the assumption of equations *)
-	constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity
-      in
-      let matx = List.rev matx in
-      let _ = assert(len = List.length lets) in
-      let env = push_rels lets env in
-      let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
-      let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
-      let args = List.rev_map (lift len) args in
-      let pred = liftn len (succ signlen) arity in
-      let pred = build_initial_predicate true allnames pred in
-
-      (* We push the initial terms to match and push their alias to rhs' envs *)
-      (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-      let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
-      let pb =
-	{ env      = env;
-	  isevars  = isevars;
-	  pred     = Some pred;
-	  tomatch  = initial_pushed;
-	  history  = start_history (List.length initial_pushed);
-	  mat      = matx;
-	  caseloc  = loc;
-	  casestyle= style;
-	  typing_function = typing_fun } in
-
-      let j = compile pb in
-	(* We check for unused patterns *)
-	List.iter (check_unused_pattern env) matx;
-	let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
-	let j =
-	  { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
-	    uj_type = nf_evar !isevars tycon; }
-	in j
-    else
-      (* We build the elimination predicate if any and check its consistency *)
-      (* with the type of arguments to match *)
-      let tmsign = List.map snd tomatchl in
-      let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
-
-      (* We push the initial terms to match and push their alias to rhs' envs *)
-      (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-      let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-      let pb =
-	{ env      = env;
-	  isevars  = isevars;
-	  pred     = pred;
-	  tomatch  = initial_pushed;
-	  history  = start_history (List.length initial_pushed);
-	  mat      = matx;
-	  caseloc  = loc;
-	  casestyle= style;
-	  typing_function = typing_fun } in
-
-      let j = compile pb in
-	(* We check for unused patterns *)
-	List.iter (check_unused_pattern env) matx;
-	inh_conv_coerce_to_tycon loc env isevars j tycon
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
deleted file mode 100644
index b7e78f6d28..0000000000
--- a/plugins/subtac/subtac_cases.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i*)
-open Errors
-open Util
-open Names
-open Term
-open Evd
-open Environ
-open Inductiveops
-open Glob_term
-open Evarutil
-(*i*)
-
-(*s Compilation of pattern-matching, subtac style. *)
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
deleted file mode 100644
index b55c43d820..0000000000
--- a/plugins/subtac/subtac_coercion.ml
+++ /dev/null
@@ -1,491 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-open Errors
-open Util
-open Names
-open Term
-open Reductionops
-open Environ
-open Typeops
-open Pretype_errors
-open Classops
-open Recordops
-open Evarutil
-open Evarconv
-open Retyping
-open Evd
-
-open Global
-open Subtac_utils
-open Coqlib
-open Printer
-open Subtac_errors
-open Eterm
-open Pp
-
-let app_opt env evars f t =
-  whd_betaiota !evars (app_opt f t)
-
-let pair_of_array a = (a.(0), a.(1))
-let make_name s = Name (id_of_string s)
-
-let rec disc_subset x =
-  match kind_of_term x with
-  | App (c, l) ->
-      (match kind_of_term c with
-      Ind i ->
-	let len = Array.length l in
-	let sig_ = delayed_force sig_ in
-	  if len = 2 && i = Term.destInd sig_.typ
-	  then
-	    let (a, b) = pair_of_array l in
-	      Some (a, b)
-	  else None
-      | _ -> None)
-  | _ -> None
-
-and disc_exist env x =
-  match kind_of_term x with
-  | App (c, l) ->
-      (match kind_of_term c with
-      Construct c ->
-	if c = Term.destConstruct (delayed_force sig_).intro
-	then Some (l.(0), l.(1), l.(2), l.(3))
-	else None
-      | _ -> None)
-  | _ -> None
-
-module Coercion = struct
-
-  exception NoSubtacCoercion
-
-  let disc_proj_exist env x =
-    match kind_of_term x with
-      | App (c, l) ->
-	  (if Term.eq_constr c (delayed_force sig_).proj1
-	     && Array.length l = 3
-	   then disc_exist env l.(2)
-	   else None)
-      | _ -> None
-
-
-  let sort_rel s1 s2 =
-    match s1, s2 with
-	Prop Pos, Prop Pos -> Prop Pos
-      | Prop Pos, Prop Null -> Prop Null
-      | Prop Null, Prop Null -> Prop Null
-      | Prop Null, Prop Pos -> Prop Pos
-      | Type _, Prop Pos -> Prop Pos
-      | Type _, Prop Null -> Prop Null
-      | _, Type _ -> s2
-
-  let hnf env isevars c = whd_betadeltaiota env isevars c
-  let hnf_nodelta env evars c = whd_betaiota evars c
-
-  let lift_args n sign =
-    let rec liftrec k = function
-      | t::sign -> liftn n k t :: (liftrec (k-1) sign)
-      | [] -> []
-    in
-      liftrec (List.length sign) sign
-
-  let rec mu env isevars t =
-    let rec aux v =
-      let v = hnf env !isevars v in
-      match disc_subset v with
-	  Some (u, p) ->
-	    let f, ct = aux u in
-	    let p = hnf env !isevars p in
-	      (Some (fun x ->
-		     app_opt env isevars 
-		     f (mkApp ((delayed_force sig_).proj1,
-			       [| u; p; x |]))),
-	       ct)
-	| None -> (None, v)
-    in aux t
-
-  and coerce loc env isevars (x : Term.constr) (y : Term.constr)
-      : (Term.constr -> Term.constr) option
-      =
-    let rec coerce_unify env x y =
-      let x = hnf env !isevars x and y = hnf env !isevars y in
-	try
-	  isevars := the_conv_x_leq env x y !isevars;
-	  None
-	with Reduction.NotConvertible -> coerce' env x y
-    and coerce' env x y : (Term.constr -> Term.constr) option =
-      let subco () = subset_coerce env isevars x y in
-      let dest_prod c =
-	match Reductionops.splay_prod_n env ( !isevars) 1 c with
-	| [(na,b,t)], c -> (na,t), c
-	| _ -> raise NoSubtacCoercion
-      in
-      let rec coerce_application typ typ' c c' l l' =
-	let len = Array.length l in
-	let rec aux tele typ typ' i co =
-	  if i < len then
-	    let hdx = l.(i) and hdy = l'.(i) in
-	      try isevars := the_conv_x_leq env hdx hdy !isevars;
-		let (n, eqT), restT = dest_prod typ in
-		let (n', eqT'), restT' = dest_prod typ' in
-		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
-	      with Reduction.NotConvertible ->
-		let (n, eqT), restT = dest_prod typ in
-		let (n', eqT'), restT' = dest_prod typ' in
-		let _ =
-		  try isevars := the_conv_x_leq env eqT eqT' !isevars
-		  with Reduction.NotConvertible -> raise NoSubtacCoercion
-		in
-		(* Disallow equalities on arities *)
-		if Reduction.is_arity env eqT then raise NoSubtacCoercion;
-		let restargs = lift_args 1
-		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
-		in
-		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
-		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
-		let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
-		let evar = make_existential loc env isevars eq in
-		let eq_app x = mkApp (delayed_force eq_rect,
-				      [| eqT; hdx; pred; x; hdy; evar|]) in
-		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
-	  else Some co
-	in
-	  if isEvar c || isEvar c' then
-	    (* Second-order unification needed. *)
-	    raise NoSubtacCoercion;
-	  aux [] typ typ' 0 (fun x -> x)
-      in
-	match (kind_of_term x, kind_of_term y) with
-	  | Sort s, Sort s' ->
-	      (match s, s' with
-		   Prop x, Prop y when x = y -> None
-		 | Prop _, Type _ -> None
-		 | Type x, Type y when x = y -> None (* false *)
-		 | _ -> subco ())
-	  | Prod (name, a, b), Prod (name', a', b') ->
-	      let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
-	      let env' = push_rel (name', None, a') env in
-	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
-		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
-	      let coec1 = app_opt env' isevars c1 (mkRel 1) in
-		(* env, x : a' |- c1[x] : lift 1 a *)
-	      let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
-		(* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
-		(match c1, c2 with
-		| None, None -> None
-		| _, _ ->
-		    Some
-		      (fun f ->
-			mkLambda (name', a',
-				 app_opt env' isevars c2
-				   (mkApp (Term.lift 1 f, [| coec1 |])))))
-
-	  | App (c, l), App (c', l') ->
-	      (match kind_of_term c, kind_of_term c' with
-		   Ind i, Ind i' -> (* Inductive types *)
-		     let len = Array.length l in
-		     let existS = delayed_force existS in
-		     let prod = delayed_force prod in
-		       (* Sigma types *)
-		       if len = Array.length l' && len = 2 && i = i'
-			 && (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
-		       then
-			 if i = Term.destInd existS.typ
-			 then
-			   begin
-			     let (a, pb), (a', pb') =
-			       pair_of_array l, pair_of_array l'
-			     in
-			     let c1 = coerce_unify env a a' in
-			     let rec remove_head a c =
-			       match kind_of_term c with
-				 | Lambda (n, t, t') -> c, t'
-				     (*| Prod (n, t, t') -> t'*)
-				 | Evar (k, args) ->
-				     let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
-				       isevars := evs;
-				       let (n, dom, rng) = destLambda t in
-				       let (domk, args) = destEvar dom in
-					 isevars := define domk a !isevars;
-					 t, rng
-				 | _ -> raise NoSubtacCoercion
-			     in
-			     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
-			     let env' = push_rel (make_name "x", None, a) env in
-			     let c2 = coerce_unify env' b b' in
-			       match c1, c2 with
-				   None, None ->
-				     None
-				 | _, _ ->
-				     Some
-				       (fun x ->
-					  let x, y =
-					    app_opt env' isevars c1 (mkApp (existS.proj1,
-							       [| a; pb; x |])),
-					    app_opt env' isevars c2 (mkApp (existS.proj2,
-							       [| a; pb; x |]))
-					  in
-					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
-			   end
-			 else
-			   begin
-			     let (a, b), (a', b') =
-			       pair_of_array l, pair_of_array l'
-			     in
-			     let c1 = coerce_unify env a a' in
-			     let c2 = coerce_unify env b b' in
-			       match c1, c2 with
-				   None, None -> None
-				 | _, _ ->
-				     Some
-				       (fun x ->
-					  let x, y =
-					    app_opt env isevars c1 (mkApp (prod.proj1,
-							       [| a; b; x |])),
-					    app_opt env isevars c2 (mkApp (prod.proj2,
-							       [| a; b; x |]))
-					  in
-					    mkApp (prod.intro, [| a'; b'; x ; y |]))
-			   end
-		       else
-			 if i = i' && len = Array.length l' then
-			   let evm =  !isevars in
-			     (try subco ()
-			       with NoSubtacCoercion ->
-				 let typ = Typing.type_of env evm c in
-				 let typ' = Typing.type_of env evm c' in
-				   (* 			     if not (is_arity env evm typ) then *)
-				   coerce_application typ typ' c c' l l')
-			       (* 			     else subco () *)
-			 else
-			   subco ()
-		 | x, y when x = y ->
-		     if Array.length l = Array.length l' then
-		       let evm =  !isevars in
-		       let lam_type = Typing.type_of env evm c in
-		       let lam_type' = Typing.type_of env evm c' in
-(* 			 if not (is_arity env evm lam_type) then ( *)
-			 coerce_application lam_type lam_type' c c' l l'
-(* 			 ) else subco () *)
-		     else subco ()
-		 | _ -> subco ())
-	  | _, _ ->  subco ()
-
-    and subset_coerce env isevars x y =
-      match disc_subset x with
-	  Some (u, p) ->
-	    let c = coerce_unify env u y in
-	    let f x =
-	      app_opt env isevars c (mkApp ((delayed_force sig_).proj1,
-				[| u; p; x |]))
-	    in Some f
-	| None ->
-	    match disc_subset y with
-		Some (u, p) ->
-		  let c = coerce_unify env x u in
-		    Some
-		      (fun x ->
-			 let cx = app_opt env isevars c x in
-			 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
-			 in
-			   (mkApp
-			      ((delayed_force sig_).intro,
-			       [| u; p; cx; evar |])))
-	      | None ->
-		  raise NoSubtacCoercion
-		    (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
-		  None*)
-    in coerce_unify env x y
-
-  let coerce_itf loc env isevars v t c1 =
-    let evars = ref isevars in
-    let coercion = coerce loc env evars t c1 in
-    let t = Option.map (app_opt env evars coercion) v in
-      !evars, t
-
-  (* Taken from pretyping/coercion.ml *)
-
-  (* Typing operations dealing with coercions *)
-
-  (* Here, funj is a coercion therefore already typed in global context *)
-  let apply_coercion_args env argl funj =
-    let rec apply_rec acc typ = function
-      | [] -> { uj_val = applist (j_val funj,argl);
-		uj_type = typ }
-      | h::restl ->
-	  (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
-  	  match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
-	    | Prod (_,c1,c2) ->
-		(* Typage garanti par l'appel à app_coercion*)
-		apply_rec (h::acc) (subst1 h c2) restl
-	    | _ -> anomaly "apply_coercion_args"
-    in
-      apply_rec [] funj.uj_type argl
-
-  (* appliquer le chemin de coercions de patterns p *)
-  exception NoCoercion
-
-  let apply_pattern_coercion loc pat p =
-    List.fold_left
-      (fun pat (co,n) ->
-	 let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
-	   Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
-      pat p
-
-  (* raise Not_found if no coercion found *)
-  let inh_pattern_coerce_to loc pat ind1 ind2 =
-    let p = lookup_pattern_path_between (ind1,ind2) in
-      apply_pattern_coercion loc pat p
-
-  (* appliquer le chemin de coercions p à hj *)
-
-  let apply_coercion env sigma p hj typ_cl =
-    try
-      fst (List.fold_left
-             (fun (ja,typ_cl) i ->
-		let fv,isid = coercion_value i in
-		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
-		let jres = apply_coercion_args env argl fv in
-		  (if isid then
-		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
-		   else
-		     jres),
-		jres.uj_type)
-             (hj,typ_cl) p)
-    with _ -> anomaly "apply_coercion"
-
-  let inh_app_fun env isevars j =
-    let isevars = ref isevars in
-    let t = hnf env !isevars j.uj_type in
-      match kind_of_term t with
-	| Prod (_,_,_) -> (!isevars,j)
-	| Evar ev when not (is_defined_evar !isevars ev) ->
-	    let (isevars',t) = define_evar_as_product !isevars ev in
-	      (isevars',{ uj_val = j.uj_val; uj_type = t })
-	| _ ->
-       	    (try
-      	       let t,p =
-		 lookup_path_to_fun_from env !isevars j.uj_type in
-		 (!isevars,apply_coercion env !isevars p j t)
-	     with Not_found ->
-	       try
-		 let coercef, t = mu env isevars t in
-		 let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
-		   (!isevars, res)
-	       with NoSubtacCoercion | NoCoercion ->
-		 (!isevars,j))
-
-  let inh_tosort_force loc env isevars j =
-    try
-      let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
-      let j1 = apply_coercion env ( isevars) p j t in
-	(isevars, type_judgment env (j_nf_evar ( isevars) j1))
-    with Not_found ->
-      error_not_a_type_loc loc env ( isevars) j
-
-  let inh_coerce_to_sort loc env isevars j =
-    let typ = hnf env isevars j.uj_type in
-      match kind_of_term typ with
-	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
-	| Evar ev when not (is_defined_evar isevars ev) ->
-	    let (isevars',s) = define_evar_as_sort isevars ev in
-	      (isevars',{ utj_val = j.uj_val; utj_type = s })
-	| _ ->
-	    inh_tosort_force loc env isevars j
-
-  let inh_coerce_to_base loc env isevars j =
-    let isevars = ref isevars in
-    let typ = hnf env !isevars j.uj_type in
-    let ct, typ' = mu env isevars typ in
-    let res =
-      { uj_val = app_opt env isevars ct j.uj_val;
-	uj_type = typ' }
-    in !isevars, res
-
-  let inh_coerce_to_prod loc env isevars t =
-    let isevars = ref isevars in
-    let typ = hnf env !isevars t in
-    let _, typ' = mu env isevars typ in
-      !isevars, typ'
-
-  let inh_coerce_to_fail env evd rigidonly v t c1 =
-    if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
-    then
-      raise NoCoercion
-    else
-    let v', t' =
-      try
-	let t2,t1,p = lookup_path_between env evd (t,c1) in
-	  match v with
-	      Some v ->
-		let j = apply_coercion env evd p
-		  {uj_val = v; uj_type = t} t2 in
-		  Some j.uj_val, j.uj_type
-	    | None -> None, t
-      with Not_found -> raise NoCoercion
-    in
-      try (the_conv_x_leq env t' c1 evd, v')
-      with Reduction.NotConvertible -> raise NoCoercion
-
-
-  let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
-    try (the_conv_x_leq env t c1 evd, v)
-    with Reduction.NotConvertible ->
-    try inh_coerce_to_fail env evd rigidonly v t c1
-    with NoCoercion ->
-    match
-      kind_of_term (whd_betadeltaiota env evd t),
-      kind_of_term (whd_betadeltaiota env evd c1)
-    with
-    | Prod (name,t1,t2), Prod (_,u1,u2) ->
-        (* Conversion did not work, we may succeed with a coercion. *)
-        (* We eta-expand (hence possibly modifying the original term!) *)
-	(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
-	(* has type forall (x:u1), u2 (with v' recursively obtained) *)
-	let name = match name with
-	  | Anonymous -> Name (id_of_string "x")
-	  | _ -> name in
-	let env1 = push_rel (name,None,u1) env in
-	let (evd', v1) =
-	  inh_conv_coerce_to_fail loc env1 evd rigidonly
-            (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
-        let v1 = Option.get v1 in
-	let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
-        let t2 = Termops.subst_term v1 t2 in
-	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
-	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
-    | _ -> raise NoCoercion
-
-  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
-    let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } 
-    and t = hnf_nodelta env evd t in
-    let (evd', val') =
-      try
-	inh_conv_coerce_to_fail loc env evd rigidonly
-	  (Some cj.uj_val) cj.uj_type t
-      with NoCoercion ->
-	(try
-	   coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
-	 with NoSubtacCoercion ->
-	   error_actual_type_loc loc env evd cj t)
-    in
-    let val' = match val' with Some v -> v | None -> assert(false) in
-      (evd',{ uj_val = val'; uj_type = t })
-	
-  let inh_conv_coerce_to = inh_conv_coerce_to_gen false
-  let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
-
-
-  let inh_conv_coerces_to loc env evd t t' =
-    try
-      fst (inh_conv_coerce_to_fail loc env evd true None t t')
-    with NoCoercion ->
-      evd (* Maybe not enough information to unify *)
-
-end
diff --git a/plugins/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli
deleted file mode 100644
index b872c99d5f..0000000000
--- a/plugins/subtac/subtac_coercion.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-open Term
-
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 6e6f42308f..33560995db 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -119,73 +119,10 @@ let interp_context_evars evdref env params =
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-(* try to find non recursive definitions *)
-
-let list_chop_hd i l = match list_chop i l with
-  | (l1,x::l2) -> (l1,x,l2)
-  | (x :: [], l2) -> ([], x, [])
-  | _ -> assert(false)
-
-let collect_non_rec env =
-  let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
-    try
-      let i =
-        list_try_find_i
-          (fun i f ->
-             if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec
-             then i else failwith "try_find_i")
-          0 lnamerec
-      in
-      let (lf1,f,lf2) = list_chop_hd i lnamerec in
-      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
-      let (lar1,ar,lar2) = list_chop_hd i larrec in
-      let newlnv =
-	try
-	  match list_chop i nrec with
-            | (lnv1,_::lnv2) -> (lnv1@lnv2)
-	    | _ -> [] (* nrec=[] for cofixpoints *)
-        with Failure "list_chop" -> []
-      in
-      searchrec ((f,def,ar)::lnonrec)
-	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
-    with Failure "try_find_i" ->
-      (List.rev lnonrec,
-       (Array.of_list lnamerec, Array.of_list ldefrec,
-        Array.of_list larrec, Array.of_list nrec))
-  in
-  searchrec []
-
-let list_of_local_binders l =
-  let rec aux acc = function
-      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
-    | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
-	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
-    | [] -> List.rev acc
-  in aux [] l
-
-let lift_binders k n l =
-  let rec aux n = function
-    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
-    | [] -> []
-  in aux n l
-
-let rec gen_rels = function
-    0 -> []
-  | n -> mkRel n :: gen_rels (pred n)
-
-let split_args n rel = match list_chop ((List.length rel) - n) rel with
-    (l1, x :: l2) -> l1, x, l2
-  | _ -> assert(false)
 
 open Coqlib
 
 let sigT = Lazy.lazy_from_fun build_sigma_type
-let sigT_info = lazy
-  { ci_ind       = destInd (Lazy.force sigT).typ;
-    ci_npar      = 2;
-    ci_cstr_ndecls = [|2|];
-    ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
-  }
 
 let rec telescope = function
   | [] -> assert false
diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
index a4b9d67e01..c932a71716 100644
--- a/plugins/subtac/subtac_plugin.mllib
+++ b/plugins/subtac/subtac_plugin.mllib
@@ -1,10 +1,7 @@
 Subtac_utils
 Eterm
 Subtac_errors
-Subtac_coercion
 Subtac_obligations
-Subtac_cases
-Subtac_pretyping_F
 Subtac_pretyping
 Subtac_command
 Subtac_classes
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
deleted file mode 100644
index 464bb8639f..0000000000
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Compat
-open Errors
-open Util
-open Names
-open Sign
-open Evd
-open Term
-open Reductionops
-open Environ
-open Type_errors
-open Typeops
-open Libnames
-open Nameops
-open Classops
-open List
-open Recordops
-open Evarutil
-open Pretype_errors
-open Glob_term
-open Evarconv
-open Pattern
-open Pretyping
-
-(************************************************************************)
-(* This concerns Cases *)
-open Declarations
-open Inductive
-open Inductiveops
-
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index cb1c9f8e1f..8f56bf52c0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -15,7 +15,6 @@ let ($) f x = f x
 (* Library linking *)
 
 let contrib_name = "Program"
-
 let subtac_dir = [contrib_name]
 let fixsub_module = subtac_dir @ ["Wf"]
 let utils_module = subtac_dir @ ["Utils"]
@@ -26,16 +25,18 @@ let init_reference dir s () = gen_reference contrib_name dir s
 let safe_init_constant md name () =
   check_required_library ("Coq"::md);
   init_constant md name ()
+let fix_proto = safe_init_constant tactics_module "fix_proto"
+let hide_obligation = safe_init_constant tactics_module "obligation"
 
 let ex_pi1 = init_constant utils_module "ex_pi1"
 let ex_pi2 = init_constant utils_module "ex_pi2"
 
 let make_ref l s = init_reference l s
+let fix_sub_ref = make_ref fixsub_module "Fix_sub"
+let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
-let fix_sub_ref = make_ref fixsub_module "Fix_sub"
-let measure_on_R_ref = make_ref fixsub_module "MR"
 let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
 let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
 
@@ -55,7 +56,6 @@ let build_sig () =
 let sig_ = build_sig
 
 let fix_proto = safe_init_constant tactics_module "fix_proto"
-
 let hide_obligation = safe_init_constant tactics_module "obligation"
 
 let eq_ind = init_constant ["Init"; "Logic"] "eq"