Fork of cases impl for subtac.

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

13 files changed, 1926 insertions, 87 deletions

diff --git a/Makefile b/Makefile
index 5d49b00b63..2f5222d98a 100644
--- a/Makefile
+++ b/Makefile
@@ -305,7 +305,7 @@ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
 SUBTACCMO=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
   contrib/subtac/g_eterm.cmo contrib/subtac/context.cmo \
   contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \
-  contrib/subtac/subtac_obligations.cmo \
+  contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \
   contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \
   contrib/subtac/subtac_interp_fixpoint.cmo \
   contrib/subtac/subtac_command.cmo contrib/subtac/subtac.cmo \
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 219cd75bac..f5115812ac 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -44,4 +44,6 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
+Ltac subtac_simpl := simpl ; intros ; destruct_exists.
+
 Extraction Inline proj1_sig.
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 4ed0b018cf..6f97a8eac6 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -38,6 +38,7 @@ struct
 		(* types *)
   let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
 
+  let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
 end
 
 open SubtacGram 
@@ -47,12 +48,17 @@ open Pcoq
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder;
+  GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt;
  
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g ] ]
     ;
 
+  subtac_nameopt:
+    [ [ "ofb"; id=Prim.ident -> Some (id) 
+      | -> None ] ]
+    ;
+
   Constr.binder_let:
     [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
@@ -76,14 +82,32 @@ let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
   (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
+type 'a nameopt_argtype = (identifier option, 'a) Genarg.abstract_argument_type
+
+let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype),
+  (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype),
+  (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) =
+  Genarg.create_arg "subtac_nameopt"
+
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
+  END
+
+VERNAC COMMAND EXTEND Subtac_Obligations
 | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
 | [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
 | [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]      
-| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]      
+| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]
+    END
+
+VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
+| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
+    END
+
+VERNAC COMMAND EXTEND Subtac_Show_Obligations
 | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
 | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
 END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index dbb0c4bdb5..fda13a12e1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -148,8 +148,10 @@ let start_proof_and_print env isevars idopt k t hook =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
+  check_required_library ["Coq";"Logic";"JMeq"];  
   require_library "Coq.subtac.FixSub";
   require_library "Coq.subtac.Utils";
+  (*Subtac_obligations.set_default_tactic (Tacinterp.lookup_tactic "subtac_simpl" []);*)
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
new file mode 100644
index 0000000000..a333cbbfe3
--- /dev/null
+++ b/contrib/subtac/subtac_cases.ml
@@ -0,0 +1,1654 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *)
+
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Inductiveops
+open Environ
+open Sign
+open Reductionops
+open Typeops
+open Type_errors
+
+open Rawterm
+open Retyping
+open Pretype_errors
+open Evarutil
+open Evarconv
+
+open Subtac_utils
+
+(* Pattern-matching errors *)
+
+type pattern_matching_error =
+  | BadPattern of constructor * constr
+  | BadConstructor of constructor * inductive
+  | WrongNumargConstructor of constructor * int
+  | WrongNumargInductive of inductive * int
+  | WrongPredicateArity of constr * constr * constr
+  | NeedsInversion of constr * constr
+  | UnusedClause of cases_pattern list
+  | NonExhaustive of cases_pattern list
+  | CannotInferPredicate of (constr * types) array
+
+exception PatternMatchingError of env * pattern_matching_error
+
+let raise_pattern_matching_error (loc,ctx,te) =
+  Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te))
+
+let error_bad_pattern_loc loc cstr ind =
+  raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
+
+let error_bad_constructor_loc loc cstr ind =
+  raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind))
+
+let error_wrong_numarg_constructor_loc loc env c n =
+  raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n))
+
+let error_wrong_numarg_inductive_loc loc env c n =
+  raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n))
+
+let error_wrong_predicate_arity_loc loc env c n1 n2 =
+  raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2))
+
+let error_needs_inversion env x t =
+  raise (PatternMatchingError (env, NeedsInversion (x,t)))
+
+module type S = sig
+  val compile_cases :
+    loc ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *
+      Evd.evar_defs ref ->
+    type_constraint -> 
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    unsafe_judgment
+end
+
+(************************************************************************)
+(*            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
+
+let push_rel_defs =
+  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
+
+(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
+   over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
+
+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         : rawconstr }
+
+type equation =
+    { patterns     : cases_pattern list; 
+      rhs          : rhs;
+      alias_stack  : name list;
+      eqn_loc      : loc;
+      used         : bool ref;
+      tag          : pattern_source }
+
+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 initial_history = function Continuation (_,[],Top) -> true | _ -> false
+
+let feed_history arg = function
+  | Continuation (n, l, h) when n>=1 ->
+      Continuation (n-1, arg :: l, h)
+  | Continuation (n, _, _) ->
+      anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
+  | Result _ -> 
+      anomaly "Exhausted pattern history"
+
+(* This is for non exhaustive error message *)
+
+let rec rawpattern_of_partial_history args2 = function
+  | Continuation (n, args1, h) ->
+      let args3 = make_anonymous_patvars (n - (List.length args2)) in
+      build_rawpattern (List.rev_append args1 (args2@args3)) h
+  | Result pl -> pl
+
+and build_rawpattern args = function
+  | Top -> args
+  | MakeAlias (AliasLeaf, rh) ->
+      assert (args = []);
+      rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+  | MakeAlias (AliasConstructor pci, rh) ->
+      rawpattern_of_partial_history
+	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
+
+let complete_history = rawpattern_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_defs ref;
+      pred     : predicate_signature option;
+      tomatch  : tomatch_stack;
+      history  : pattern_continuation;
+      mat      : matrix;
+      caseloc  : loc;
+      typing_function: type_constraint -> env -> rawconstr -> 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
+
+
+module Cases_F(Coercion : Coercion.S) : S = struct
+
+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 (Evd.evars_of !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_rawconstr 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_rawconstr tomatch) env !isevars j in
+  isevars := evd;
+  let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+  let t =
+    try IsInd (typ,find_rectype env (Evd.evars_of !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 (Evd.evars_of !(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) (mk_tycon_type indt)).uj_val in
+	    let sigma = Evd.evars_of !(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
+
+let lift_tomatch n ((current,typ),info) =
+  ((lift n current,lift_tomatch_type n typ),info)
+
+(**********************************************************************)
+(* 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 unalias_pat = function
+  | PatVar (c,name) as p ->
+      if name = Anonymous then p else PatVar (c,Anonymous)
+  | PatCstr(a,b,c,name) as p ->
+      if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
+
+let remove_current_pattern eqn =
+  match eqn.patterns with
+    | pat::pats ->
+	{ 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 }
+
+(**********************************************************************)
+(* Dealing with regular and default patterns *)
+let is_regular eqn = eqn.tag = RegularPat
+
+let lower_pattern_status = function
+  | RegularPat -> DefaultPat 0
+  | DefaultPat n -> DefaultPat (n+1)
+
+let pattern_status pats =
+  if array_exists ((=) RegularPat) pats then RegularPat
+  else 
+    let min =
+      Array.fold_right
+	(fun pat n -> match pat with
+	   | DefaultPat i when i<n -> i
+	   | _ -> n)
+	pats 0 in
+    DefaultPat min
+
+(**********************************************************************)
+(* 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 Closure.mind_equiv env 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.tag, eqn.rhs
+
+(**********************************************************************)
+(* Functions to deal with matrix factorization *)
+
+let occur_in_rhs na rhs =
+  match na with
+    | Anonymous -> false
+    | Name id -> occur_rawconstr 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 t = mkRel (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 liftn_rel_declaration n k = map_rel_declaration (liftn n k)
+let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
+
+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 push_rels_eqn sign eqn =
+  {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env} }
+
+let push_rels_eqn_with_names sign eqn =
+  let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
+  let sign = recover_alias_names alias_of_pat pats sign in
+  push_rels_eqn sign eqn
+
+let build_aliases_context env sigma names allpats pats =
+  (* pats is the list of bodies to push as an alias *)
+  (* They all are defined in env and we turn them into a sign *)
+  (* cuts in sign need to be done in allpats *)
+  let rec insert env sign1 sign2 n newallpats oldallpats = function
+    | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) ->
+        (* Anonymous leaves must be considered named and treated in the *)
+        (* next clause because they may occur in implicit arguments *)
+	insert env sign1 sign2
+	  n newallpats (List.map List.tl oldallpats) (pats,names)
+    | (deppat,nondeppat,d,t)::pats, na::names ->
+	let nondeppat = lift n nondeppat in
+	let deppat = lift n deppat in
+	let newallpats =
+	  List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
+	let oldallpats = List.map List.tl oldallpats in
+	let decl = (na,Some deppat,t) in
+	let a = (deppat,nondeppat,d,t) in
+	insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) 
+	  newallpats oldallpats (pats,names)
+    | [], [] -> newallpats, sign1, sign2, env
+    | _ -> anomaly "Inconsistent alias and name lists" in
+  let allpats = List.map (fun x -> [x]) allpats
+  in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names)
+
+let insert_aliases_eqn sign eqnnames alias_rest eqn =
+  let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
+  { eqn with
+      alias_stack = alias_rest;
+      rhs = {eqn.rhs with rhs_env = push_rels thissign eqn.rhs.rhs_env}}
+	    
+
+let insert_aliases env sigma alias eqns =
+  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
+  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
+  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
+  let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
+  let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
+  (* 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) (Evd.evars_of 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
+  lam_it 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_betaevar empty_env (Evd.evars_of !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 (evars_of 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 (Evd.evars_of !isevars) indf current tms p
+      | None -> infer_predicate loc env isevars typs cstrs indf in
+  let typ = whd_beta (applist (pred, realargs)) in
+  if dep then
+    (pred, whd_beta (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 args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
+		 let rest = {rest with tag = lower_pattern_status rest.tag} 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
+	trace (str "In generalize_problem");
+	debug 4 (str "Generalize problem: decl " ++ my_print_context (push_rel d pb.env));
+      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 tag, rhs = extract_rhs pb in
+  let tycon = match pb.pred with
+    | None -> empty_tycon
+    | Some (PrCcl typ) -> mk_tycon typ
+    | Some _ -> anomaly "not all parameters of pred have been consumed" in
+  tag, 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
+
+  sign,
+  { pb with
+      env = push_rels sign pb.env;
+      tomatch = List.rev_append currents tomatch;
+      pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.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 tags   = Array.map (fun (t,_,_) -> t) brs in
+	  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 RegularStyle tags in
+	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+	  let inst = List.map mkRel deps in
+	    debug 4 (str "Building app: " ++ my_print_constr pb.env (applist (case, inst)) ++
+		    str " for deps " ++ str (string_of_list "," string_of_int deps));
+	  pattern_status tags,
+	  { 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 tag, j = compile pb in
+  (tag, 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
+  debug 4 (str "Compile generalization: " ++ my_print_env pb.env);
+  let patstat,j = compile pb in
+  patstat, 
+  { 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 (Evd.evars_of !(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 patstat,j = compile pb in
+  patstat, 
+  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 tomatchl eqns =
+  let build_eqn (loc,ids,lpat,rhs) =
+    let initial_lpat,initial_rhs = lpat,rhs in
+    let initial_rhs = rhs in
+    let rhs =
+      { rhs_env = env;
+	avoid_ids = ids@(ids_of_named_context (named_context env));
+	it = initial_rhs } in
+    { patterns = initial_lpat;
+      tag = RegularPat;
+      alias_stack = [];
+      eqn_loc = loc;
+      used = ref false;
+      rhs = rhs }
+  in List.map build_eqn eqns
+
+(************************************************************************)
+(* preparing the elimination predicate if any                          *)
+
+let build_expected_arity env isevars isdep tomatchl =
+  let cook n = function
+    | _,IsInd (_,IndType(indf,_)) ->
+        let indf' = lift_inductive_family n indf in
+	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
+    | _,NotInd _ -> None
+  in
+  let rec buildrec n env = function
+    | [] -> new_Type ()
+    | tm::ltm ->
+	match cook n tm with
+	  | None -> buildrec n env ltm
+	  | Some (ty1,aritysign) ->
+	      let rec follow n env = function
+		| d::sign ->
+		    mkProd_or_LetIn_name env
+		      (follow (n+1) (push_rel d env) sign) d
+		| [] ->
+		    if isdep then
+		      mkProd (Anonymous, ty1, 
+			      buildrec (n+1)
+				(push_rel_assum (Anonymous, ty1) env)
+				ltm)
+		    else buildrec n env ltm
+	      in follow n env (List.rev aritysign)
+  in buildrec 0 env tomatchl
+
+let extract_predicate_conclusion isdep tomatchl pred =
+  let cook = function
+    | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
+    | _,NotInd _ -> None in
+  let rec decomp_lam_force n l p =
+    if n=0 then (l,p) else
+    match kind_of_term p with
+      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
+      | _ -> (* eta-expansion *)
+          let na = Name (id_of_string "x") in
+          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
+  let rec buildrec allnames p = function
+    | [] -> (List.rev allnames,p)
+    | tm::ltm ->
+	match cook tm with
+	  | None -> 
+              let p = 
+                (* adjust to a sign containing the NotInd's *)
+                if isdep then lift 1 p else p in
+              let names = if isdep then [Anonymous] else [] in
+              buildrec (names::allnames) p ltm
+	  | Some n ->
+              let n = if isdep then n+1 else n in
+              let names,p = decomp_lam_force n [] p in
+              buildrec (names::allnames) p ltm
+  in buildrec [] pred tomatchl
+
+let set_arity_signature dep n arsign tomatchl pred x =
+  (* avoid is not exhaustive ! *)
+  let rec decomp_lam_force n avoid l p =
+    if n = 0 then (List.rev l,p,avoid) else
+    match p with
+      | RLambda (_,(Name id as na),_,c) -> 
+          decomp_lam_force (n-1) (id::avoid) (na::l) c
+      | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c
+      | _ ->
+          let x = next_ident_away (id_of_string "x") avoid in
+          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+          (* eta-expansion *)
+            (let a = RVar (dummy_loc,x) in
+             match p with
+               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+               | _ -> (RApp (dummy_loc,p,[a]))) in
+  let rec decomp_block avoid p = function
+    | ([], _) -> x := Some p
+    | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l')  ->
+	let (ind,params) = dest_ind_family indf in
+        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
+        in
+        let na,p,avoid' = 
+          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
+        in 
+        y :=
+        (List.hd na,
+         if List.for_all ((=) Anonymous) nal then
+           None
+         else
+           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
+        decomp_block avoid' p (l,l')
+    | (_::l),(y::l') ->
+        y := (Anonymous,None);
+        decomp_block avoid p (l,l')
+    | _ -> anomaly "set_arity_signature"
+  in
+  decomp_block [] pred (tomatchl,arsign)
+
+let prepare_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 (Evd.evars_of !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 (evars_of 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 (Evd.evars_of !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',nparams,realnal) ->
+		  if ind <> ind' then
+		    user_err_loc (loc,"",str "Wrong inductive type");
+		  if List.length params <> nparams
+		    or nrealargs <> List.length realnal then
+		      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 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
+
+
+(* 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 prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
+  (* No type annotation *)
+  | None ->
+      (match tycon with
+       | Some (None, t) ->
+	   let names,pred = 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
+	   in Some (build_initial_predicate false names pred)
+       | _ -> None)
+
+  (* Some type annotation *)
+  | Some rtntyp ->
+      (* We extract the signature of the arity *)
+      let arsign = extract_arity_signature env tomatchs sign in
+      let env = List.fold_right push_rels arsign env in
+      let allnames = List.rev (List.map (List.map pi1) arsign) in
+      let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+      let _ = 
+	option_map (fun tycon -> 
+		      let tycon' = (lift_tycon_type (succ (List.length arsign)) tycon) in
+			isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val
+			  tycon')
+	  tycon
+      in
+      let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+	Some (build_initial_predicate true allnames predccl)
+
+(**************************************************************************)
+(* Main entry of the matching compilation                                 *)
+  
+let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+  
+  (* We build the matrix of patterns and right-hand-side *)
+  let matx = matx_of_eqns env tomatchl eqns in
+    
+  (* We build the vector of terms to match consistently with the *)
+  (* constructors found in patterns *)
+  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+    
+  (* 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 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;
+      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
+end
+  
diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli
new file mode 100644
index 0000000000..9e90212670
--- /dev/null
+++ b/contrib/subtac/subtac_cases.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Evd
+open Environ
+open Inductiveops
+open Rawterm
+open Evarutil
+(*i*)
+
+type pattern_matching_error =
+  | BadPattern of constructor * constr
+  | BadConstructor of constructor * inductive
+  | WrongNumargConstructor of constructor * int
+  | WrongNumargInductive of inductive * int
+  | WrongPredicateArity of constr * constr * constr
+  | NeedsInversion of constr * constr
+  | UnusedClause of cases_pattern list
+  | NonExhaustive of cases_pattern list
+  | CannotInferPredicate of (constr * types) array
+
+exception PatternMatchingError of env * pattern_matching_error
+
+val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
+
+val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
+
+(*s Compilation of pattern-matching. *)
+
+module type S = sig
+  val compile_cases :
+    loc ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+    type_constraint -> 
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    unsafe_judgment
+end
+
+module Cases_F(C : Coercion.S) : S
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4691afb157..ba85e705e8 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -224,7 +224,7 @@ module Coercion = struct
 			 if len = 1 && len = Array.length l' && i = i' then
 			   let argx, argy = l.(0), l'.(0) in
 			   let indtyp = Inductiveops.type_of_inductive env i in
-			   let argname, argtype, rest = destProd indtyp in
+			   let argname, argtype, _ = destProd indtyp in
 			   let eq =
 			     mkApp (Lazy.force eqind, [| argtype; argx; argy |])
 			   in
@@ -391,7 +391,7 @@ module Coercion = struct
        debug 1 (str "inh_conv_coerce_to_fail called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++
 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
-	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+	      Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
     try (the_conv_x_leq env t c1 isevars, v, t)
@@ -457,7 +457,7 @@ module Coercion = struct
        debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
-	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+	      Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
     match n with
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 7a1c403232..5312fb3311 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -31,6 +31,13 @@ type program_info = {
   prg_deps : (identifier * int) list;
 }
 
+let assumption_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+
+let set_default_tactic t = default_tactic := t
+
 let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
 			     evar_concl = o.obl_type ; 
 			     evar_body = Evar_empty ;
@@ -277,7 +284,8 @@ let subtac_obligation (user_num, name, typ) =
 			 let obls = Array.copy obls in
 			 let _ = obls.(num) <- obl in
 			   update_obls prg obls (pred rem));
-		    trace (str "Started obligation " ++ int user_num ++ str "  proof")
+		      Pfedit.by !default_tactic;
+		      trace (str "Started obligation " ++ int user_num ++ str "  proof")
      		 | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		     ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)))
 	  | Some r -> error "Obligation already solved"
@@ -317,6 +325,22 @@ let solve_obligations n tac =
   in
     update_obls prg obls' !rem
 
+let admit_obligations n =
+  let prg = get_prog n in
+  let obls, rem = prg.prg_obligations in
+  let obls' = 
+    Array.mapi (fun i x -> 
+		 match x.obl_body with 
+		     None -> 
+			 let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+			   assumption_message x.obl_name;
+			   { x with obl_body = Some (mkConst kn) }
+		   | Some _ -> x)
+      obls
+  in
+    update_obls prg obls' 0
+
+
 open Pp
 let show_obligations n =
   let prg = get_prog n in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 07f151697a..972aadce6d 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -2,6 +2,8 @@ open Util
 
 type obligation_info = (Names.identifier * Term.types * Intset.t) array
 
+val set_default_tactic : Proof_type.tactic -> unit
+
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   obligation_info -> unit
 
@@ -13,3 +15,5 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit
+
+val admit_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index f550ac73e8..cd639e7784 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -40,7 +40,7 @@ open Inductiveops
 
 module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
-  module Cases = Cases.Cases_F(Coercion)
+  module Cases = Subtac_cases.Cases_F(Coercion)
 
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   let allow_anonymous_refs = ref true
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d476b4cd8d..7b7b66c217 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -50,6 +50,16 @@ let eqrec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
 let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
 let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
 
+let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
+let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+
+let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq")
+let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec")
+let jmeq_ind_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq")
+let jmeq_refl_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq_refl")
+
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
 
@@ -88,7 +98,7 @@ let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
-let debug_level = 1
+let debug_level = 4
 
 let debug_on = true
 
@@ -426,66 +436,72 @@ let make_discr (loc, po, tml, eqns) =
       eqns
   i
 *)
-let rewrite_cases_aux (loc, po, tml, eqns) =
-  let tml = list_mapi (fun i (c, (n, opt)) -> c, 
-		       ((match n with
-			    Name id -> (match c with
-					  | RVar (_, id') when id = id' ->
-					      Name (id_of_string (string_of_id id ^ "'"))
-					  | _ -> n)
-			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
-			opt)) tml 
-  in
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
-		       [mkHole; c; n])
-  in
-  let eqs_types = 
-    List.map
-      (fun (c, (n, _)) ->
-	 let id = match n with Name id -> id | _ -> assert false in
-	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
-	   Name heqid, mkeq c (RVar (dummy_loc, id)))
-      tml
-  in
-  let po = 
-    List.fold_right
-      (fun (n,t) acc ->
-	 RProd (dummy_loc, Anonymous, t, acc))
-      eqs_types (match po with 
-		     Some e -> e
-		   | None -> mkHole)
-  in
-  let eqns =   
-    List.map (fun (loc, idl, cpl, c) ->
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
-			      [mkHole; c])
-  in
-  let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
-  let case = RCases (loc,Some po,tml,eqns) in
-  let app = RApp (dummy_loc, case, refls) in
-    app
-
-let rec rewrite_cases c = 
-  match c with 
-      RCases _ -> let c' = map_rawconstr rewrite_cases c in
-	(match c' with 
-	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
-	   | _ -> assert(false))
-    | _ -> map_rawconstr rewrite_cases c
+(* let rewrite_cases_aux (loc, po, tml, eqns) = *)
+(*   let tml = list_mapi (fun i (c, (n, opt)) -> c,  *)
+(* 		       ((match n with *)
+(* 			    Name id -> (match c with *)
+(* 					  | RVar (_, id') when id = id' -> *)
+(* 					      Name (id_of_string (string_of_id id ^ "'")) *)
+(* 					  | _ -> n) *)
+(* 			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))), *)
+(* 			opt)) tml  *)
+(*   in *)
+(*   let mkHole = RHole (dummy_loc, InternalHole) in *)
+(*   (\* let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)), *\) *)
+(* (\* 		       [mkHole; c; n]) *\) *)
+(* (\*   in *\) *)
+(*   let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqdep_ind_ref)), *)
+(* 		       [mkHole; c; mkHole; n]) *)
+(*   in *)
+(*   let eqs_types =  *)
+(*     List.map *)
+(*       (fun (c, (n, _)) -> *)
+(* 	 let id = match n with Name id -> id | _ -> assert false in *)
+(* 	 let heqid = id_of_string ("Heq" ^ string_of_id id) in *)
+(* 	   Name heqid, mkeq c (RVar (dummy_loc, id))) *)
+(*       tml *)
+(*   in *)
+(*   let po =  *)
+(*     List.fold_right *)
+(*       (fun (n,t) acc -> *)
+(* 	 RProd (dummy_loc, Anonymous, t, acc)) *)
+(*       eqs_types (match po with  *)
+(* 		     Some e -> e *)
+(* 		   | None -> mkHole) *)
+(*   in *)
+(*   let eqns =    *)
+(*     List.map (fun (loc, idl, cpl, c) -> *)
+(* 		let c' =  *)
+(* 		  List.fold_left  *)
+(* 		    (fun acc (n, t) -> *)
+(* 		       RLambda (dummy_loc, n, mkHole, acc)) *)
+(* 		    c eqs_types *)
+(* 		in (loc, idl, cpl, c')) *)
+(*       eqns *)
+(*   in *)
+(*   let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
+(* 			      [mkHole; c]) *)
+(*   in *)
+(*   (\*let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
+(* 			      [mkHole; c]) *)
+(*   in*\) *)
+(*   let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in *)
+(*   let case = RCases (loc,Some po,tml,eqns) in *)
+(*   let app = RApp (dummy_loc, case, refls) in *)
+(*     app *)
+
+(* let rec rewrite_cases c =  *)
+(*   match c with  *)
+(*       RCases _ -> let c' = map_rawconstr rewrite_cases c in *)
+(* 	(match c' with  *)
+(* 	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) *)
+(* 	   | _ -> assert(false)) *)
+(*     | _ -> map_rawconstr rewrite_cases c *)
 	  
-let rewrite_cases env c =
-  let c' = rewrite_cases c in
-  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
-    c'
+(* let rewrite_cases env c = *)
+(*   let c' = rewrite_cases c in *)
+(*   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *)
+(*     c' *)
 
 let list_mapi f = 
   let rec aux i = function 
@@ -511,8 +527,8 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
   in
   let mkHole = RHole (dummy_loc, InternalHole) in
   let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
-		       [mkHole; c; n])
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force jmeq_ind_ref)),
+		       [mkHole; c; mkHole; n])
   in
   let eqs_types = 
     List.map
@@ -539,7 +555,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
 		in (loc, idl, cpl, c'))
       eqns
   in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force jmeq_refl_ref),
 			      [mkHole; c])
   in
   let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
@@ -559,10 +575,11 @@ let rec rewrite_cases c =
 	   | _ -> assert(false))
     | _ -> map_rawconstr rewrite_cases c
 	  
-let rewrite_cases env c =
+let rewrite_cases env c = c
+(*
   let c' = rewrite_cases c in
   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
-    c'
+    c'*)
 
 let id_of_name = function
     Name n -> n
@@ -616,3 +633,69 @@ let rec string_of_list sep f = function
 
 let string_of_intset d = 
   string_of_list "," string_of_int (Intset.elements d)
+
+(**********************************************************)
+(* Pretty-printing *)
+open Printer
+open Ppconstr
+open Nameops
+open Termops
+open Evd
+
+let pr_meta_map evd =
+  let ml = meta_list evd in
+  let pr_name = function
+      Name id -> str"[" ++ pr_id id ++ str"]"
+    | _ -> mt() in
+  let pr_meta_binding = function
+    | (mv,Cltyp (na,b)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name na ++ str " : " ++
+           print_constr b.rebus ++ fnl ())
+    | (mv,Clval(na,b,_)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name na ++ str " := " ++
+             print_constr (fst b).rebus ++ fnl ())
+  in
+  prlist pr_meta_binding ml    
+
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+
+let pr_evar_info evi =
+  let phyps = 
+    (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
+    Printer.pr_named_context (Global.env()) (evar_context evi)
+  in
+  let pty = print_constr evi.evar_concl in
+  let pb =
+    match evi.evar_body with
+      | Evar_empty -> mt ()
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+  in
+  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
+
+let pr_evar_map sigma =
+  h 0 
+    (prlist_with_sep pr_fnl
+      (fun (ev,evi) ->
+        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+      (to_list sigma))
+
+let pr_constraints pbs =
+  h 0
+    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+      print_constr t1 ++ spc() ++
+      str (match pbty with
+	| Reduction.CONV -> "=="
+	| Reduction.CUMUL -> "<=") ++ 
+      spc() ++ print_constr t2) pbs)
+
+let pr_evar_defs evd =
+  let pp_evm =
+    let evars = evars_of evd in
+    if evars = empty then mt() else
+      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
+  let pp_met =
+    if meta_list evd = [] then mt() else
+      str"METAS:"++brk(0,1)++pr_meta_map evd in
+  v 0 (pp_evm ++ pp_met)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a0d9f6f56f..0cdbc757ab 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -31,10 +31,17 @@ val proj1_sig_ref : reference
 val proj2_sig_ref : reference
 val build_sig : unit -> coq_sigma_data
 val sig_ : coq_sigma_data lazy_t
+
 val eqind : constr lazy_t
 val eqrec : constr lazy_t
 val eqind_ref : global_reference lazy_t
 val refl_equal_ref : global_reference lazy_t
+
+val eqdep_ind : constr lazy_t
+val eqdep_rec : constr lazy_t
+val eqdep_ind_ref : global_reference lazy_t
+val eqdep_intro_ref : global_reference lazy_t
+
 val boolind : constr lazy_t
 val sumboolind : constr lazy_t
 val natind : constr lazy_t
@@ -49,6 +56,7 @@ val acc : constr lazy_t
 val acc_inv : constr lazy_t
 val extconstr : constr -> constr_expr
 val extsort : sorts -> constr_expr
+
 val my_print_constr : env -> constr -> std_ppcmds
 val my_print_constr_expr : constr_expr -> std_ppcmds
 val my_print_evardefs : evar_defs -> std_ppcmds
@@ -100,3 +108,5 @@ val solve_by_tac : evar_info -> Tacmach.tactic -> constr
 
 val string_of_list : string -> ('a -> string) -> 'a list -> string
 val string_of_intset : Intset.t -> string
+
+val pr_evar_defs : evar_defs -> Pp.std_ppcmds
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 55e5e90352..8fedeed516 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,17 +1,3 @@
-Print eq_rec.
-Print eq.
-Inductive vector : nat -> Set :=
-  | vnil : vector 0
-  | vcons : nat -> forall n, vector n -> vector (S n).
-Set Printing All.
-Print eq.
-Program Fixpoint vapp (n m : nat) (v : vector n) (w : vector m) { struct v } : vector (n + m) :=
-  match v with
-  | vnil => w
-  | vcons a n' v' => vcons a (n' + m) (vapp n' m v' w)
-  end.
-
-
 Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.
 Require Import Coq.Arith.Compare_dec.