Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

17 files changed, 1552 insertions, 337 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
new file mode 100644
index 00000000..9d120019
--- /dev/null
+++ b/contrib/subtac/equations.ml4
@@ -0,0 +1,1149 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(************************************************************************)
+(*  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 camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*) 
+
+(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *)
+
+open Cases
+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 List
+open Libnames
+
+type pat =
+  | PRel of int
+  | PCstr of constructor * pat list
+  | PInac of constr
+
+let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern")
+  
+let mkInac env c =
+  mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |])
+    
+let rec constr_of_pat ?(inacc=true) env = function
+  | PRel i -> mkRel i
+  | PCstr (c, p) -> 
+      let c' = mkConstruct c in
+	mkApp (c', Array.of_list (constrs_of_pats ~inacc env p))
+  | PInac r -> 
+      if inacc then try mkInac env r with _ -> r else r
+      
+and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l
+
+let rec pat_vars = function
+  | PRel i -> Intset.singleton i
+  | PCstr (c, p) -> pats_vars p
+  | PInac _ -> Intset.empty
+
+and pats_vars l = 
+  fold_left (fun vars p -> 
+    let pvars = pat_vars p in
+    let inter = Intset.inter pvars vars in
+      if inter = Intset.empty then
+	Intset.union pvars vars
+      else error ("Non-linear pattern: variable " ^
+		     string_of_int (Intset.choose inter) ^ " appears twice"))
+    Intset.empty l
+
+let rec pats_of_constrs l = map pat_of_constr l
+and pat_of_constr c = 
+  match kind_of_term c with
+  | Rel i -> PRel i
+  | App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) ->
+      PInac c
+  | App (f, args) when isConstruct f ->
+      PCstr (destConstruct f, pats_of_constrs (Array.to_list args))
+  | Construct f -> PCstr (f, [])
+  | _ -> PInac c
+
+let inaccs_of_constrs l = map (fun x -> PInac x) l
+
+exception Conflict
+
+let rec pmatch p c =
+  match p, c with
+  | PRel i, t -> [i, t]
+  | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl'
+  | PInac _, _ -> []
+  | _, PInac _ -> []
+  | _, _ -> raise Conflict
+
+and pmatches pl l =
+  match pl, l with
+  | [], [] -> []
+  | hd :: tl, hd' :: tl' -> 
+      pmatch hd hd' @ pmatches tl tl'
+  | _ -> raise Conflict
+      
+let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
+
+let rec pinclude p c =
+  match p, c with
+  | PRel i, t -> true
+  | PCstr (c, pl), PCstr (c', pl') when c = c' -> pincludes pl pl'
+  | PInac _, _ -> true
+  | _, PInac _ -> true
+  | _, _ -> false
+      
+and pincludes pl l =
+  match pl, l with
+  | [], [] -> true
+  | hd :: tl, hd' :: tl' -> 
+      pinclude hd hd' && pincludes tl tl'
+  | _ -> false
+      
+let pattern_includes pl l = pincludes pl l
+
+(** Specialize by a substitution. *)
+
+let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s)
+
+let subst_rel_subst k s c = 
+  let rec aux depth c =
+    match kind_of_term c with
+    | Rel n -> 
+	let k = n - depth in 
+	  if k >= 0 then 
+	    try lift depth (snd (assoc k s))
+	    with Not_found -> c
+	  else c
+    | _ -> map_constr_with_binders succ aux depth c
+  in aux k c
+    
+let subst_context s ctx =
+  let (_, ctx') = fold_right 
+    (fun (id, b, t) (k, ctx') ->
+      (succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx'))
+    ctx (0, [])
+  in ctx'
+
+let subst_rel_context k cstr ctx = 
+  let (_, ctx') = fold_right 
+    (fun (id, b, t) (k, ctx') ->
+      (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
+    ctx (k, [])
+  in ctx'
+
+let rec lift_pat n k p = 
+  match p with
+  | PRel i ->
+      if i >= k then PRel (i + n)
+      else p
+  | PCstr(c, pl) -> PCstr (c, lift_pats n k pl)
+  | PInac r -> PInac (liftn n k r)
+      
+and lift_pats n k = map (lift_pat n k)
+
+let rec subst_pat env k t p = 
+  match p with
+  | PRel i -> 
+      if i = k then t
+      else if i > k then PRel (pred i)
+      else p
+  | PCstr(c, pl) ->
+      PCstr (c, subst_pats env k t pl)
+  | PInac r -> PInac (substnl [constr_of_pat ~inacc:false env t] (pred k) r)
+
+and subst_pats env k t = map (subst_pat env k t)
+
+let rec specialize s p = 
+  match p with
+  | PRel i -> 
+      if mem_assoc i s then
+	let b, t = assoc i s in
+	  if b then PInac t
+	  else PRel (destRel t)
+      else p
+  | PCstr(c, pl) ->
+      PCstr (c, specialize_pats s pl)
+  | PInac r -> PInac (specialize_constr s r)
+
+and specialize_constr s c = subst_rel_subst 0 s c
+and specialize_pats s = map (specialize s)
+
+let specialize_patterns = function
+  | [] -> fun p -> p
+  | s -> specialize_pats s
+
+let specialize_rel_context s ctx =
+  snd (fold_right (fun (n, b, t) (k, ctx) -> 
+    (succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx))
+	  ctx (0, []))
+    
+let lift_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
+
+type program = 
+  signature * clause list
+
+and signature = identifier * rel_context * constr
+
+and clause = lhs * (constr, int) rhs
+
+and lhs = rel_context * identifier * pat list
+
+and ('a, 'b) rhs = 
+  | Program of 'a
+  | Empty of 'b
+
+type splitting = 
+  | Compute of clause
+  | Split of lhs * int * inductive_family *
+      unification_result array * splitting option array
+      
+and unification_result = 
+  rel_context * int * constr * pat * substitution option
+
+and substitution = (int * (bool * constr)) list
+
+type problem = identifier * lhs
+
+let rels_of_tele tele = rel_list 0 (List.length tele)
+
+let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele)
+
+let split_solves split prob =
+  match split with
+  | Compute (lhs, rhs) -> lhs = prob
+  | Split (lhs, id, indf, us, ls) -> lhs = prob
+
+let ids_of_constr c = 
+  let rec aux vars c = 
+    match kind_of_term c with
+    | Var id -> Idset.add id vars
+    | _ -> fold_constr aux vars c
+  in aux Idset.empty c
+
+let ids_of_constrs = 
+  fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
+
+let idset_of_list =
+  fold_left (fun s x -> Idset.add x s) Idset.empty
+
+let intset_of_list =
+  fold_left (fun s x -> Intset.add x s) Intset.empty
+
+let solves split (delta, id, pats as prob) = 
+  split_solves split prob && 
+  Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta)))
+
+let check_judgment ctx c t =
+  ignore(Typing.check (push_rel_context ctx (Global.env ())) Evd.empty c t); true
+
+let check_context env ctx =
+  fold_right
+    (fun (_, _, t as decl) env -> 
+      ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
+    ctx env
+
+let split_context n c =
+  let after, before = list_chop n c in
+    match before with
+    | hd :: tl -> after, hd, tl
+    | [] -> raise (Invalid_argument "split_context")
+	
+let split_tele n (ctx : rel_context) =
+  let rec aux after n l =
+    match n, l with
+    | 0, decl :: before -> before, decl, List.rev after
+    | n, decl :: before -> aux (decl :: after) (pred n) before
+    | _ -> raise (Invalid_argument "split_tele")
+  in aux [] n ctx
+
+let rec add_var_subst env subst n c =
+  if mem_assoc n subst then
+    let t = assoc n subst in
+      if eq_constr t c then subst
+      else unify env subst t c
+  else 
+    let rel = mkRel n in
+      if rel = c then subst
+      else if dependent rel c then raise Conflict
+      else (n, c) :: subst
+    
+and unify env subst x y =
+  match kind_of_term x, kind_of_term y with
+  | Rel n, _ -> add_var_subst env subst n y
+  | _, Rel n -> add_var_subst env subst n x
+  | App (c, l), App (c', l') when eq_constr c c' ->
+      unify_constrs env subst (Array.to_list l) (Array.to_list l')
+  | _, _ -> if eq_constr x y then subst else raise Conflict
+
+and unify_constrs (env : env) subst l l' = 
+  if List.length l = List.length l' then
+    fold_left2 (unify env) subst l l'
+  else raise Conflict
+
+let fold_rel_context_with_binders f ctx init =
+  snd (List.fold_right (fun decl (depth, acc) ->
+    (succ depth, f depth decl acc)) ctx (0, init))
+    
+let dependent_rel_context (ctx : rel_context) k =
+  fold_rel_context_with_binders
+    (fun depth (n,b,t) acc -> 
+      let r = mkRel (depth + k) in
+	acc || dependent r t ||
+	  (match b with
+	  | Some b -> dependent r b
+	  | None -> false))
+    ctx false
+
+let liftn_between n k p c =
+  let rec aux depth c = match kind_of_term c with
+    | Rel i -> 
+	if i <= depth then c
+	else if i-depth > p then c
+	else mkRel (i - n)
+    | _ -> map_constr_with_binders succ aux depth c
+  in aux k c
+    
+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 substnl_rel_context n l =
+  map_rel_context_with_binders (fun k -> substnl l (n+k-1))
+
+let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list) =
+  let _, s, ctx' =
+    fold_left (fun (k, s, ctx') (n, b, t as decl) ->
+      match b with
+      | None -> (succ k, mkRel k :: s, ctx' @ [decl])
+      | Some t -> (k, lift (pred k) t :: map (substnl [t] (pred k)) s, subst_rel_context 0 t ctx'))
+      (1, [], []) ctx
+  in
+  let s = rev s in
+  let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in
+    s', ctx'
+      
+(* Compute the transitive closure of the dependency relation for a term in a context *)
+
+let rec dependencies_of_rel ctx k =
+  let (n,b,t) = nth ctx (pred k) in
+  let b = Option.map (lift k) b and t = lift k t in
+  let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in
+    Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t))
+      
+and dependencies_of_term ctx t =
+  let rels = free_rels t in
+    Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty
+
+let subst_telescope k cstr ctx = 
+  let (_, ctx') = fold_left
+    (fun (k, ctx') (id, b, t) ->
+      (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
+    (k, []) ctx
+  in rev ctx'
+
+let lift_telescope n k sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign)
+    | [] -> []
+  in liftrec k sign
+    
+type ('a,'b) either = Inl of 'a | Inr of 'b
+  
+let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
+  let rels = dependencies_of_term ctx t in
+  let len = length ctx in
+  let nbdeps = Intset.cardinal rels in
+  let lifting = len - nbdeps in (* Number of variables not linked to t *)
+  let rec aux k n acc m rest s = function
+    | decl :: ctx' ->
+	if Intset.mem k rels then
+	  let rest' = subst_telescope 0 (mkRel (nbdeps + lifting - pred m)) rest in
+	    aux (succ k) (succ n) (decl :: acc) m rest' ((k, Inl n) :: s) ctx'
+	else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
+    | [] -> rev acc, rev rest, s
+  in aux 1 1 [] 1 [] [] ctx
+    
+let merge_subst (ctx', rest, s) =
+  let lenrest = length rest in
+    map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s
+
+(* let simplify_subst s =  *)
+(*   fold_left (fun s (k, t) ->  *)
+(*     match kind_of_term t with *)
+(*     | Rel n when n = k -> s *)
+(*     | _ -> (k, t) :: s) *)
+(*     [] s *)
+
+let compose_subst s' s =
+  map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s
+
+let substitute_in_ctx n c ctx =
+  let rec aux k after = function
+    | [] -> []
+    | (name, b, t as decl) :: before ->
+	if k = n then rev after @ (name, Some c, t) :: before
+	else aux (succ k) (decl :: after) before
+  in aux 1 [] ctx
+    
+let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) =
+  match cursubst with
+  | [] -> ctx, substacc
+  | (k, (b, t)) :: rest ->
+      if t = mkRel k then reduce_subst ctx substacc rest
+      else if noccur_between 1 k t then
+	(* The term to substitute refers only to previous variables. *)
+	let t' = lift (-k) t in
+	let ctx' = substitute_in_ctx k t' ctx in
+	  reduce_subst ctx' substacc rest
+      else (* The term refers to variables declared after [k], so we have 
+	      to move these dependencies before [k]. *)
+	let (minctx, ctxrest, subst as str) = strengthen ctx t in
+	  match assoc k subst with
+	  | Inl _ -> error "Occurs check in substituted_context"
+	  | Inr k' ->
+	      let s = merge_subst str in
+	      let ctx' = ctxrest @ minctx in
+	      let rest' =
+		let substsubst (k', (b, t')) =
+		  match kind_of_term (snd (assoc k' s)) with
+		  | Rel k'' -> (k'', (b, specialize_constr s t'))
+		  | _ -> error "Non-variable substituted for variable by strenghtening"
+		in map substsubst ((k, (b, t)) :: rest)
+	      in
+		reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *)
+		  
+		  
+let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
+  let _, subst =
+    fold_left (fun (k, s) _ ->
+      try let t = assoc k subst in
+	    (succ k, (k, (true, t)) :: s)
+      with Not_found ->
+	(succ k, ((k, (false, mkRel k)) :: s)))
+      (1, []) ctx
+  in
+  let ctx', subst' = reduce_subst ctx subst subst in
+    reduce_rel_context ctx' subst'
+    
+let unify_type before ty =
+  try
+    let envb = push_rel_context before (Global.env()) in
+    let IndType (indf, args) = find_rectype envb Evd.empty ty in
+    let ind, params = dest_ind_family indf in
+    let vs = map (Reduction.whd_betadeltaiota envb) args in
+    let cstrs = Inductiveops.arities_of_constructors envb ind in
+    let cstrs = 
+      Array.mapi (fun i ty ->
+	let ty = prod_applist ty params in
+	let ctx, ty = decompose_prod_assum ty in
+	let ctx, ids = 
+	  let ids = ids_of_rel_context ctx in
+	    fold_right (fun (n, b, t as decl) (acc, ids) ->
+	      match n with Name _ -> (decl :: acc), ids
+	      | Anonymous -> let id = next_name_away Anonymous ids in
+			       ((Name id, b, t) :: acc), (id :: ids))
+	      ctx ([], ids)
+	in
+	let env' = push_rel_context ctx (Global.env ()) in
+	let IndType (indf, args) = find_rectype env' Evd.empty ty in
+	let ind, params = dest_ind_family indf in
+	let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in
+	let constrpat = PCstr ((ind, succ i), inaccs_of_constrs params @ patvars_of_tele ctx) in
+	  env', ctx, constr, constrpat, (* params @  *)args)
+	cstrs
+    in
+    let res = 
+      Array.map (fun (env', ctxc, c, cpat, us) -> 
+	let _beforelen = length before and ctxclen = length ctxc in
+	let fullctx = ctxc @ before in
+	  try
+	    let fullenv = push_rel_context fullctx (Global.env ()) in
+	    let vs' = map (lift ctxclen) vs in
+	    let subst = unify_constrs fullenv [] vs' us in
+	    let subst', ctx' = substituted_context subst fullctx in
+	      (ctx', ctxclen, c, cpat, Some subst')
+	  with Conflict -> 
+	    (fullctx, ctxclen, c, cpat, None)) cstrs
+    in Some (res, indf)
+  with Not_found -> (* not an inductive type *)
+    None
+
+let rec id_of_rel n l =
+  match n, l with
+  | 0, (Name id, _, _) :: tl -> id
+  | n, _ :: tl -> id_of_rel (pred n) tl
+  | _, _ -> raise (Invalid_argument "id_of_rel")
+
+let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) = 
+  constrs_of_pats ~inacc (push_rel_context ctx env) pats
+      
+let rec valid_splitting (f, delta, t, pats) tree = 
+  split_solves tree (delta, f, pats) && 
+    valid_splitting_tree (f, delta, t) tree
+    
+and valid_splitting_tree (f, delta, t) = function
+  | Compute (lhs, Program rhs) -> 
+      let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in 
+	ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true
+
+  | Compute ((ctx, id, lhs), Empty split) -> 
+      let before, (x, _, ty), after = split_context split ctx in
+      let unify = 
+	match unify_type before ty with
+	| Some (unify, _) -> unify 
+	| None -> assert false
+      in
+	array_for_all (fun (_, _, _, _, x) -> x = None) unify
+	  
+  | Split ((ctx, id, lhs), rel, indf, unifs, ls) -> 
+      let before, (id, _, ty), after = split_tele (pred rel) ctx in
+      let unify, indf' = Option.get (unify_type before ty) in
+	assert(indf = indf');
+	if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false
+	else
+	  let ok, splits = 
+	    Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) -> 
+	      match subst with
+	      | None -> acc
+	      | Some subst ->
+(* 		  let env' = push_rel_context ctx' (Global.env ()) in *)
+(* 		  let ctx_correct =  *)
+(* 		    ignore(check_context env' (subst_context subst ctxc)); *)
+(* 		    ignore(check_context env' (subst_context subst before)); *)
+(* 		    true *)
+(* 		  in  *)
+		  let newdelta = 
+		    subst_context subst (subst_rel_context 0 cstr 
+					    (lift_contextn ctxlen 0 after)) @ before in
+		  let liftpats = lift_pats ctxlen rel lhs in
+		  let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
+		    (ok, (f, newdelta, newpats) :: splits))
+	      (true, []) unify
+	  in
+	  let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta 
+	    (constrs_of_pats ~inacc:false (Global.env ()) lhs) 
+	  in
+	  let t' = replace_vars subst t in
+	    ok && for_all 
+	      (fun (f, delta', pats') -> 
+		array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits
+	      
+let valid_tree (f, delta, t) tree = 
+  valid_splitting (f, delta, t, patvars_of_tele delta) tree
+
+let is_constructor c =
+  match kind_of_term (fst (decompose_app c)) with
+  | Construct _ -> true
+  | _ -> false
+
+let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
+  let rec find_split_pat curpat patc =
+    match patc with
+    | PRel _ -> None
+    | PCstr (f, args) ->
+	(match curpat with
+	| PCstr (f', args') when f = f' -> (* Already split at this level, continue *)
+	    find_split_pats args' args
+	| PRel i -> (* Split on i *) Some i
+	| PInac c when isRel c -> Some (destRel c)
+	| _ -> None)
+    | PInac _ -> None
+
+  and find_split_pats curpats patcs =
+    assert(List.length curpats = List.length patcs);
+    fold_left2 (fun acc -> 
+      match acc with
+      | None -> find_split_pat | _ -> fun _ _ -> acc)
+      None curpats patcs
+  in find_split_pats curpats patcs
+      
+open Pp
+open Termops
+
+let pr_constr_pat env c =
+  let pr = print_constr_env env c in
+    match kind_of_term c with
+    | App _ -> str "(" ++ pr ++ str ")"
+    | _ -> pr
+
+let pr_pat env c =
+  try 
+    let patc = constr_of_pat env c in
+      try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception"
+  with _ -> str"constr_of_pat raised an exception"
+    
+let pr_context env c =
+  let pr_decl (id,b,_) = 
+    let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in
+    let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in
+      idstr ++ bstr
+  in
+    prlist_with_sep pr_spc pr_decl (List.rev c)
+(*   Printer.pr_rel_context env c *)
+
+let pr_lhs env (delta, f, patcs) =
+  let env = push_rel_context delta env in
+  let ctx = pr_context env delta in
+    (if delta = [] then ctx else str "[" ++ ctx ++ str "]" ++ spc ())
+    ++ pr_id f ++ spc () ++ prlist_with_sep spc (pr_pat env) patcs
+
+let pr_rhs env = function
+  | Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var)
+  | Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs
+      
+let pr_clause env (lhs, rhs) =
+  pr_lhs env lhs ++ 
+    (let env' = push_rel_context (pi1 lhs) env in
+       pr_rhs env' rhs)
+    
+(* let pr_splitting env = function *)
+(*   | Compute cl -> str "Compute " ++ pr_clause env cl *)
+(*   | Split (lhs, n, indf, results, splits) -> *)
+
+(* let pr_unification_result (ctx, n, c, pat, subst) = *)
+  
+(*       unification_result array * splitting option array *)
+
+let pr_clauses env =
+  prlist_with_sep fnl (pr_clause env)
+
+let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
+  pattern_includes patcs patcs'
+    
+let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
+  pattern_matches patcs patcs'
+
+let rec split_on env var (delta, f, curpats as lhs) clauses =
+  let before, (id, _, ty), after = split_tele (pred var) delta in
+  let unify, indf = 
+    match unify_type before ty with 
+    | Some r -> r
+    | None -> assert false (* We decided... so it better be inductive *)
+  in
+  let clauses = ref clauses in
+  let splits = 
+    Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) ->
+      match s with
+      | None -> None
+      | Some s -> 
+	  (* ctx' |- s cstr, s cstrpat *)
+	  let newdelta =
+	    subst_context s (subst_rel_context 0 cstr 
+				(lift_contextn ctxlen 1 after)) @ ctx' in
+	  let liftpats = 
+	    (* delta |- curpats -> before; ctxc; id; after |- liftpats *)
+	    lift_pats ctxlen (succ var) curpats 
+	  in
+	  let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *)
+	    lift_pat (pred var) 1 cstrpat
+	  in
+	  let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *)
+	    subst_pats env var liftpat liftpats 
+	  in
+	  let lifts = (* before; ctxc |- s : newdelta ->
+			 before; ctxc; after |- lifts : newdelta ; after *)
+	    map (fun (k,(b,x)) -> (pred var + k, (b, lift (pred var) x))) s
+	  in
+	  let newpats = specialize_patterns lifts substpat in
+	  let newlhs = (newdelta, f, newpats) in
+	  let matching, rest = 
+	    fold_right (fun (lhs, rhs as clause) (matching, rest) -> 
+	      if lhs_includes newlhs lhs then
+		(clause :: matching, rest)
+	      else (matching, clause :: rest))
+	      !clauses ([], [])
+	  in
+	    clauses := rest;
+	    if matching = [] then (
+	      (* Try finding a splittable variable *)
+	      let (id, _) = 
+		fold_right (fun (id, _, ty as decl) (accid, ctx) -> 
+		  match accid with 
+		  | Some _ -> (accid, ctx)
+		  | None -> 
+		      match unify_type ctx ty with
+		      | Some (unify, indf) ->
+			  if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
+			    (Some id, ctx)
+			  else (None, decl :: ctx)
+		      | None -> (None, decl :: ctx))
+		  newdelta (None, [])
+	      in 
+		match id with
+		| None ->
+		    errorlabstrm "deppat"
+	      	      (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
+	      		  pr_lhs env newlhs)
+		| Some id -> 
+		    Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta))))
+	    ) else (
+	      let splitting = make_split_aux env newlhs matching in
+		Some splitting))
+      unify
+  in
+(*     if !clauses <> [] then *)
+(*       errorlabstrm "deppat" *)
+(* 	(str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *)
+    Split (lhs, var, indf, unify, splits)
+      
+and make_split_aux env lhs clauses =
+  let split = 
+    fold_left (fun acc (lhs', rhs) -> 
+      match acc with 
+      | None -> find_split lhs lhs'
+      | _ -> acc) None clauses
+  in 
+    match split with
+    | Some var -> split_on env var lhs clauses
+    | None ->
+	(match clauses with
+	| [] -> error "No clauses left"
+	| [(lhs', rhs)] ->
+	    (* No need to split anymore, fix the environments so that they are correctly aligned. *)
+	    (match lhs_matches lhs' lhs with
+	    | Some s ->
+		let s = map (fun (x, p) -> x, (true, constr_of_pat ~inacc:false env p)) s in
+		let rhs' = match rhs with
+		  | Program c -> Program (specialize_constr s c)
+		  | Empty i -> Empty (destRel (snd (assoc i s)))
+		in Compute ((pi1 lhs, pi2 lhs, specialize_patterns s (pi3 lhs')), rhs')
+	    | None -> anomaly "Non-matching clauses at a leaf of the splitting tree")
+	| _ ->
+	    errorlabstrm "make_split_aux"
+	      (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses))
+
+let make_split env (f, delta, t) clauses =
+  make_split_aux env (delta, f, patvars_of_tele delta) clauses
+    
+open Evd
+open Evarutil
+
+let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s
+let map_substitution s t = map (subst_rel_subst 0 s) t
+
+let term_of_tree status isevar env (i, delta, ty) ann tree =
+(*   let envrec = match ann with *)
+(*     | None -> [] *)
+(*     | Some (loc, i) ->  *)
+(* 	let (n, t) = lookup_rel_id i delta in *)
+(* 	let t' = lift n t in *)
+	  
+	  
+(*   in *)
+  let rec aux = function
+    | Compute ((ctx, _, pats as lhs), Program rhs) -> 
+	let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
+	let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in
+	  mkCast(body, DEFAULTcast, typ), typ
+
+    | Compute ((ctx, _, pats as lhs), Empty split) ->
+	let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
+	let split = (Name (id_of_string "split"), 
+		    Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))),
+		    Lazy.force Class_tactics.coq_nat)
+	in
+	let ty' = it_mkProd_or_LetIn ty' ctx in
+	let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in
+	let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in
+	  term, ty'
+	    
+    | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) -> 
+	let before, decl, after = split_tele (pred rel) ctx in
+	let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
+	let branches = 
+	  array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split -> 
+	    match split with
+	    | Some s -> aux s
+	    | None -> 
+		(* dead code, inversion will find a proof of False by splitting on the rel'th hyp *)
+		Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat)
+	    unif sp 
+	in
+	let branches_ctx =
+	  Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt))
+	    branches
+	in
+	let n, branches_lets = 
+	  Array.fold_left (fun (n, lets) (id, b, t) -> 
+	    (succ n, (Name id, Option.map (lift n) b, lift n t) :: lets))
+	    (0, []) branches_ctx
+	in
+	let liftctx = lift_contextn (Array.length branches) 0 ctx in
+	let case =
+	  let ty = it_mkProd_or_LetIn ty' liftctx in
+	  let ty = it_mkLambda_or_LetIn ty branches_lets in
+	  let nbbranches = (Name (id_of_string "branches"), 
+			   Some (Class_tactics.coq_nat_of_int (length branches_lets)),
+			   Lazy.force Class_tactics.coq_nat)
+	  in
+	  let nbdiscr = (Name (id_of_string "target"), 
+			Some (Class_tactics.coq_nat_of_int (length before)),
+			Lazy.force Class_tactics.coq_nat)
+	  in
+	  let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in
+	  let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in
+	    term
+	in       
+	let casetyp = it_mkProd_or_LetIn ty' ctx in
+	  mkCast(case, DEFAULTcast, casetyp), casetyp
+
+  in aux tree
+
+open Topconstr
+open Constrintern
+open Decl_kinds
+
+type equation = constr_expr * (constr_expr, identifier located) rhs
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> true
+    | SyntacticDef kn -> true
+
+let is_global id =
+  try 
+    locate_reference (make_short_qualid id)
+  with Not_found -> 
+    false
+
+let is_freevar ids env x =
+  try
+    if Idset.mem x ids then false
+    else
+      try ignore(Environ.lookup_named x env) ; false
+      with _ -> not (is_global x)
+  with _ -> true
+  
+let ids_of_patc c ?(bound=Idset.empty) l = 
+  let found id bdvars l =
+    if not (is_freevar bdvars (Global.env ()) (snd id)) then l
+    else if List.exists (fun (_, id') -> id' = snd id) l then l 
+    else id :: l 
+  in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident lid) -> found lid bdvars l
+    | CNotation (_, "{ _ : _ | _ }", ((CRef (Ident (_, id))) :: _, _)) when not (Idset.mem id bdvars) ->
+	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+  in aux bound l c
+
+let interp_pats i isevar env impls pat sign recu =
+  let bound = Idset.singleton i in
+  let vars = ids_of_patc pat ~bound [] in
+  let varsctx, env' = 
+    fold_right (fun (loc, id) (ctx, env) ->
+      let decl =
+	let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in
+	  (Name id, None, ty) 
+      in
+	decl::ctx, push_rel decl env)
+      vars ([], env)
+  in
+  let pats =
+    let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
+    let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
+      match kind_of_term patt with
+      | App (m, args) -> 
+	  if not (eq_constr m (mkRel (succ (length varsctx)))) then
+	    user_err_loc (constr_loc pat, "interp_pats",
+			 str "Expecting a pattern for " ++ pr_id i)
+	  else Array.to_list args
+      | _ -> user_err_loc (constr_loc pat, "interp_pats",
+			  str "Error parsing pattern: unnexpected left-hand side")
+  in
+    isevar := nf_evar_defs !isevar;
+    (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, 
+    nf_env_evar (Evd.evars_of !isevar) env',
+    rev_map (nf_evar (Evd.evars_of !isevar)) pats)
+      
+let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
+  let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
+  let rhs' = match rhs with
+    | Program p -> 
+	let ty = nf_isevar !isevar (substl patcs arity) in
+	  Program (interp_casted_constr_evars isevar env' ~impls p ty)
+    | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
+  in ((ctx, i, pats_of_constrs (rev patcs)), rhs')	
+
+open Entries
+
+open Tacmach
+open Tacexpr
+open Tactics
+open Tacticals
+
+let contrib_tactics_path =
+  make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"])
+
+let tactics_tac s =
+  make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)
+    
+let equations_tac = lazy 
+  (Tacinterp.eval_tactic 
+      (TacArg(TacCall(dummy_loc, 
+		     ArgArg(dummy_loc, tactics_tac "equations"), []))))
+
+let define_by_eqs with_comp i (l,ann) t nt eqs =
+  let env = Global.env () in
+  let isevar = ref (create_evar_defs Evd.empty) in
+  let (env', sign), impls = interp_context_evars isevar env l in
+  let arity = interp_type_evars isevar env' t in
+  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
+  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let arity = 
+    if with_comp then
+      let compid = add_suffix i "_comp" in
+      let ce =
+	{ const_entry_body = it_mkLambda_or_LetIn arity sign;
+	  const_entry_type = None;
+	  const_entry_opaque = false;
+	  const_entry_boxed = false} 
+      in
+      let c =
+	Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
+      in mkApp (mkConst c, rel_vect 0 (length sign))
+    else arity
+  in
+  let env = Global.env () in
+  let ty = it_mkProd_or_LetIn arity sign in
+  let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
+  let fixdecls = [(Name i, None, ty)] in
+  let fixenv = push_rel_context fixdecls env in
+  let equations = 
+    States.with_heavy_rollback (fun () -> 
+      Option.iter (Command.declare_interning_data data) nt;
+      map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
+  in
+  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
+  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let prob = (i, sign, arity) in
+  let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
+  let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in
+    (*   let ce = check_evars fixenv Evd.empty !isevar in *)
+    (*   List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
+  let is_recursive, env' =
+    let occur_eqn ((ctx, _, _), rhs) =
+      match rhs with
+      | Program c -> dependent (mkRel (succ (length ctx))) c
+      | _ -> false
+    in if exists occur_eqn equations then true, fixenv else false, env
+  in
+  let split = make_split env' prob equations in
+    (* if valid_tree prob split then *)
+  let status = (* if is_recursive then Expand else *) Define false in
+  let t, ty = term_of_tree status isevar env' prob ann split in
+  let undef = undefined_evars !isevar in
+  let t, ty = if is_recursive then 
+    (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls)
+    else t, ty
+  in
+  let obls, t', ty' = 
+    Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty
+  in
+    if is_recursive then
+      ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] [] 
+		~tactic:(Lazy.force equations_tac)
+		(Command.IsFixpoint [None, CStructRec]))
+    else
+      ignore(Subtac_obligations.add_definition
+		~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls)
+      
+module Gram = Pcoq.Gram
+module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
+
+module DeppatGram =
+struct
+  let gec s = Gram.Entry.create ("Deppat."^s)
+
+  let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
+
+  let binders_let2 : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e = gec "binders_let2"
+
+(*   let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *)
+
+end
+
+open Rawterm
+open DeppatGram 
+open Util
+open Pcoq
+open Prim
+open Constr
+open G_vernac
+
+GEXTEND Gram
+  GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
+ 
+  deppat_equations:
+    [ [ l = LIST1 equation SEP ";" -> l ] ]
+  ;
+
+  binders_let2:
+    [ [ l = binders_let_fixannot -> l ] ]
+  ;
+
+  equation:
+    [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ]
+  ;
+
+  rhs:
+    [ [ ":=!"; id = identref -> Empty id
+      |":="; c = Constr.lconstr -> Program c
+    ] ]
+  ;
+  
+  END
+
+type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
+
+let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
+  (globwit_deppat_equations : Genarg.glevel deppat_equations_argtype),
+  (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
+  Genarg.create_arg "deppat_equations"
+
+type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type
+
+let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
+  (globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
+  (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
+  Genarg.create_arg "binders_let2"
+
+type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type
+
+let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
+  (globwit_decl_notation : Genarg.glevel decl_notation_argtype),
+  (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
+  Genarg.create_arg "decl_notation"
+
+let equations wc i l t nt eqs =
+  try define_by_eqs wc i l t nt eqs
+  with e -> msg (Cerrors.explain_exn e)
+
+VERNAC COMMAND EXTEND Define_equations
+| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
+      decl_notation(nt) ] ->
+    [ equations true i l t nt eqs ]
+      END
+
+VERNAC COMMAND EXTEND Define_equations2
+| [ "Equations_nocomp" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
+      decl_notation(nt) ] ->
+    [ equations false i l t nt eqs ]
+END
+    
+let rec int_of_coq_nat c = 
+  match kind_of_term c with
+  | App (f, [| arg |]) -> succ (int_of_coq_nat arg)
+  | _ -> 0
+
+let solve_equations_goal destruct_tac tac gl =
+  let concl = pf_concl gl in
+  let targetn, branchesn, targ, brs, b =
+    match kind_of_term concl with
+    | LetIn (Name target, targ, _, b) ->
+	(match kind_of_term b with
+	| LetIn (Name branches, brs, _, b) ->
+	    target, branches, int_of_coq_nat targ, int_of_coq_nat brs, b
+	| _ -> error "Unnexpected goal")
+    | _ -> error "Unnexpected goal"
+  in
+  let branches, b = 
+    let rec aux n c =
+      if n = 0 then [], c
+      else match kind_of_term c with
+      | LetIn (Name id, br, brt, b) -> 
+	  let rest, b = aux (pred n) b in
+	    (id, br, brt) :: rest, b
+      | _ -> error "Unnexpected goal"
+    in aux brs b
+  in 
+  let ids = targetn :: branchesn :: map pi1 branches in
+  let cleantac = tclTHEN (intros_using ids) (thin ids) in
+  let dotac = tclDO (succ targ) intro in
+  let subtacs = 
+    tclTHENS destruct_tac
+      (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches)
+  in tclTHENLIST [cleantac ; dotac ; subtacs] gl
+    
+TACTIC EXTEND solve_equations
+  [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ]
+    END
+
+let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
+let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
+
+let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
+
+let specialize_hyp id gl =
+  let env = pf_env gl in
+  let ty = pf_get_hyp_typ gl id in
+  let evars = ref (create_evar_defs (project gl)) in
+  let rec aux in_eqs acc ty =
+    match kind_of_term ty with
+    | Prod (_, t, b) -> 
+	(match kind_of_term t with
+	| App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
+	    let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in
+	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; x |]) in
+	      if e_conv env evars pt t then
+		aux true (mkApp (acc, [| p |])) (subst1 p b)
+	      else error "Unconvertible members of an homogeneous equality"
+	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+	    let pt = mkApp (Lazy.force coq_heq, [| eqty; x; eqty; x |]) in
+	    let p = mkApp (Lazy.force coq_heq_refl, [| eqty; x |]) in
+	      if e_conv env evars pt t then
+		aux true (mkApp (acc, [| p |])) (subst1 p b)
+	      else error "Unconvertible members of an heterogeneous equality"
+	| _ -> 
+	    if in_eqs then acc, in_eqs, ty
+	    else 
+	      let e = e_new_evar evars env t in
+		aux false (mkApp (acc, [| e |])) (subst1 e b))
+    | t -> acc, in_eqs, ty
+  in 
+  try 
+    let acc, worked, ty = aux false (mkVar id) ty in
+    let ty = Evarutil.nf_isevar !evars ty in
+      if worked then
+	tclTHENFIRST
+	  (fun g -> Tacmach.internal_cut true id ty g)
+	  (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
+      else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
+  with e -> tclFAIL 0 (Cerrors.explain_exn e) gl
+      
+TACTIC EXTEND specialize_hyp
+[ "specialize_hypothesis" constr(c) ] -> [ 
+  match kind_of_term c with
+  | Var id -> specialize_hyp id
+  | _ -> tclFAIL 0 (str "Not an hypothesis") ]
+END
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9bfb33ea..00a69bba 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
@@ -6,12 +7,14 @@
 *)
 
 open Term
+open Sign
 open Names
 open Evd
 open List
 open Pp
 open Util
 open Subtac_utils
+open Proof_type
 
 let trace s = 
   if !Flags.debug then (msgnl s; msgerr s)
@@ -20,15 +23,27 @@ let trace s =
 let succfix (depth, fixrels) = 
   (succ depth, List.map succ fixrels)
 
+type oblinfo =
+  { ev_name: int * identifier;
+    ev_hyps: named_context;
+    ev_status: obligation_definition_status;
+    ev_chop: int option;
+    ev_loc: Util.loc;
+    ev_typ: types;
+    ev_tac: Tacexpr.raw_tactic_expr option;
+    ev_deps: Intset.t }
+    
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
+
 let subst_evar_constr evs n t = 
   let seen = ref Intset.empty in
   let transparent = ref Idset.empty in
   let evar_info id = List.assoc id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
-	let (id, idstr), hyps, chop, _, _, _ = 
+	let { ev_name = (id, idstr) ; 
+	      ev_hyps = hyps ; ev_chop = chop } =
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -46,17 +61,13 @@ let subst_evar_constr evs n t =
 	  let rec aux hyps args acc =
 	     match hyps, args with
 		 ((_, None, _) :: tlh), (c :: tla) -> 
-		   aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc)
+		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
 	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
 	  in aux hyps args [] 
 	in
-  	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++
-			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
-			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
- 	   with _ -> ());
 	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
 	    transparent := Idset.add idstr !transparent;
 	  mkApp (mkVar idstr, Array.of_list args)
@@ -93,8 +104,8 @@ let etype_of_evar evs hyps concl =
 	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
-		if noccurn 1 rest then lift (-1) rest, s', trans'
-		else
+(* 		if noccurn 1 rest then lift (-1) rest, s', trans' *)
+(* 		else *)
 		  let c', s'', trans'' = subst_evar_constr evs n c in
 		  let c' = subst_vars acc 0 c' in
 		    mkNamedProd_or_LetIn (id, Some c', t'') rest, 
@@ -121,15 +132,34 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations env name isevars evm fs t ty = 
-  (* 'Serialize' the evars, we assume that the types of the existentials
-     refer to previous existentials in the list only *)
-  trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
-  trace (str "Term given to eterm" ++ spc () ++
-	    Termops.print_constr_env (Global.env ()) t);
+let evar_dependencies evm ev =
+  let one_step deps = 
+    Intset.fold (fun ev s -> 
+      let evi = Evd.find evm ev in
+	Intset.union (Evarutil.evars_of_evar_info evi) s)
+      deps deps
+  in 
+  let rec aux deps =
+    let deps' = one_step deps in
+      if Intset.equal deps deps' then deps
+      else aux deps'
+  in aux (Intset.singleton ev)
+
+let sort_dependencies evl =
+  List.sort (fun (_, _, deps) (_, _, deps') -> 
+    if Intset.subset deps deps' then (* deps' depends on deps *) -1
+    else if Intset.subset deps' deps then 1
+    else Intset.compare deps deps')
+    evl
+    
+let eterm_obligations env name isevars evm fs ?status t ty = 
+  (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
   let nc_len = Sign.named_context_length nc in
   let evl = List.rev (to_list evm) in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
@@ -146,20 +176,29 @@ let eterm_obligations env name isevars evm fs t ty =
 	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
 	 let evtyp, hyps, chop = 
 	   match chop_product fs evtyp with
-	       Some t -> 
-		 (try
-		    trace (str "Choped a product: " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) t);
-		  with _ -> ());
-		 t, trunc_named_context fs hyps, fs
-	     | None -> evtyp, hyps, 0
+	   | Some t -> t, trunc_named_context fs hyps, fs
+	   | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id isevars in
-	 let opacity = match k with QuestionMark o -> o | _ -> true in
-	 let opaque = if not opacity || chop <> fs then None else Some chop in
-	 let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in
-	   y' :: l) 
+	 let status = match k with QuestionMark o -> Some o | _ -> status in
+	 let status, chop = match status with 
+	   | Some (Define true as stat) ->
+	       if chop <> fs then Define false, None 
+	       else stat, Some chop
+	   | Some s -> s, None
+	   | None -> Define true, None
+	 in
+	 let tac = match ev.evar_extra with 
+	   | Some t -> 
+	       if Dyn.tag t = "tactic" then 
+		 Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
+	       else None
+	   | None -> None
+	 in
+	 let info = { ev_name = (n, nstr);
+		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
+		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+	 in (id, info) :: l) 
       evn []
   in 
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
@@ -167,28 +206,16 @@ let eterm_obligations env name isevars evm fs t ty =
   in
   let ty, _, _ = subst_evar_constr evts 0 ty in
   let evars = 
-    List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> 
-      name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
-  in
-    (try
-       trace (str "Term constructed in eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t');
-       ignore(iter
-		(fun (name, typ, _, _, deps) ->
-		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
-			    Termops.print_constr_env (Global.env ()) typ))
-		evars);
-     with _ -> ());
-    Array.of_list (List.rev evars), t', ty
+    List.map (fun (_, info) ->
+      let { ev_name = (_, name); ev_status = status;
+	    ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+      in
+      let status = match status with
+	| Define true when Idset.mem name transparent -> Define false
+	| _ -> status
+      in name, typ, loc, status, deps, tac) evts
+  in Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
-(* let eterm evm t (tycon : types option) =  *)
-(*   let t, tycon, evs = eterm_term evm t tycon in *)
-(*     match tycon with *)
-(* 	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *)
-(*       | None -> Tactics.apply_term t (mkMetas (List.length evs)) *)
-     
-(* open Tacmach *)
-
 let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index 007e327c..19e8ffe8 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -6,23 +6,27 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: eterm.mli 10889 2008-05-06 14:05:20Z msozeau $ i*)
+(*i $Id: eterm.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 open Environ
 open Tacmach
 open Term
 open Evd
 open Names
 open Util
+open Tacinterp
 
 val mkMetas : int -> constr list
 
-(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
-
-(* env, id, evars, number of
-   function prototypes to try to clear from evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> 
-  (identifier * types * loc * bool * Intset.t) array * constr * types
-    (* Obl. name, type as product, location of the original evar, 
-       opacity (true = opaque) and dependencies as indexes into the array *)
+val evar_dependencies : evar_map -> int -> Intset.t
+val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
+  
+(* env, id, evars, number of function prototypes to try to clear from
+   evars contexts, object and type *)
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> 
+  ?status:obligation_definition_status -> constr -> types -> 
+  (identifier * types * loc * obligation_definition_status * Intset.t * 
+      Tacexpr.raw_tactic_expr option) array * constr * types
+    (* Obl. name, type as product, location of the original evar, associated tactic,
+       status and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 4cf5336d..7194d435 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -14,7 +14,7 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
-(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: g_subtac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 
 open Flags
@@ -112,25 +112,25 @@ END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligation
 | [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" ] -> 
-    [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ]
+    [ Subtac_obligations.try_solve_obligations None None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
 | [ "Solve" "All" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ]
+    [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ]
 | [ "Solve" "All" "Obligations" ] -> 
-    [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ]
+    [ Subtac_obligations.solve_all_obligations None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Admit_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 7bfa107b..ba00fce5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
 
 open Global
 open Pp
@@ -52,16 +52,14 @@ open Tacexpr
 let solve_tccs_in_type env id isevars evm c typ =
   if not (evm = Evd.empty) then 
     let stmt_id = Nameops.add_suffix id "_stmt" in
-    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
-    (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
-    let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
+    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
-	  Subtac_obligations.Defined cst -> constant_value (Global.env()) 
-	    (match cst with ConstRef kn -> kn | _ -> assert false)
-	| _ -> 
-	    errorlabstrm "start_proof" 
-	      (str "The statement obligations could not be resolved automatically, " ++ spc () ++
-		  str "write a statement definition first.")
+      Subtac_obligations.Defined cst -> constant_value (Global.env()) 
+	(match cst with ConstRef kn -> kn | _ -> assert false)
+      | _ -> 
+	  errorlabstrm "start_proof" 
+	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+		str "write a statement definition first.")
   else
     let _ = Typeops.infer_type env c in c
 
@@ -106,12 +104,9 @@ let declare_assumption env isevars idl is_coe k bl c nl =
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
 
-let dump_definition (loc, id) s =
-  Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
-
 let dump_constraint ty ((loc, n), _, _) =
   match n with
-    | Name id -> dump_definition (loc, id) ty
+    | Name id -> Dumpglob.dump_definition (loc, id) false ty
     | Anonymous -> ()
 
 let dump_variable lid = ()
@@ -119,9 +114,9 @@ let dump_variable lid = ()
 let vernac_assumption env isevars kind l nl =
   let global = fst kind = Global in
     List.iter (fun (is_coe,(idl,c)) -> 
-      if !Flags.dump then
+      if Dumpglob.dump () then
 	List.iter (fun lid -> 
-	  if global then dump_definition lid "ax" 
+	  if global then Dumpglob.dump_definition lid (not global) "ax"
 	  else dump_variable lid) idl;
       declare_assumption env isevars idl is_coe kind [] c nl) l
 
@@ -139,7 +134,7 @@ let subtac (loc, command) =
   match command with
   | VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
       check_fresh lid;
-      dump_definition lid "def";
+      Dumpglob.dump_definition lid false "def";
       (match expr with
       | ProveBody (bl, t) -> 
 	  if Lib.is_modtype () then
@@ -152,12 +147,12 @@ let subtac (loc, command) =
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
-	dump_definition lid "fix") l;
+	Dumpglob.dump_definition lid false "fix") l;
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l b)
 	  
   | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
-      if !Flags.dump then dump_definition id "prf";
+      Dumpglob.dump_definition id false "prf";
       if not(Pfedit.refining ()) then
 	if lettop then
 	  errorlabstrm "Subtac_command.StartProof"
@@ -172,11 +167,12 @@ let subtac (loc, command) =
       vernac_assumption env isevars stre l nl
 	
   | VernacInstance (glob, sup, is, props, pri) ->
-      if !Flags.dump then dump_constraint "inst" is;
+      dump_constraint "inst" is;
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 	
   | VernacCoFixpoint (l, b) ->
-      List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
+      if Dumpglob.dump () then 
+	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
       ignore(Subtac_command.build_corecursive l b)
 	
   (*| VernacEndProof e -> 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 04bf54d3..094226ff 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: subtac_cases.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 open Cases
 open Util
@@ -1572,7 +1572,7 @@ let mk_JMeq typ x typ' y =
   mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
-let hole = RHole (dummy_loc, Evd.QuestionMark true)
+let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
 let context_of_arsign l =
   let (x, _) = List.fold_right
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 9a5539e2..0d44a0c0 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -92,104 +92,103 @@ let type_class_instance_params isevars env id n ctx inst subst =
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri =
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
-  let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass =
     match bk with
-      | Implicit ->
-	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = class_info (Nametab.global id) in
-	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
-	    if needlen <> applen then 
-	      Classes.mismatched_params env (List.map fst par) (List.map snd k.cl_context);
-	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
-	      (fun avoid (clname, (id, _, t)) -> 
-		match clname with 
-		    Some (cl, b) -> 
-		      let t = 
-			if b then 
-			  let _k = class_info cl in
-			    CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *)
-			else CHole (Util.dummy_loc, None)
-		      in t, avoid
-		  | None -> failwith ("new instance: under-applied typeclass"))
-	      par (List.rev k.cl_context)
-	    in Topconstr.CAppExpl (loc, (None, id), pars)
-
+    | Implicit ->
+	Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
+	  ~allow_partial:false (fun avoid (clname, (id, _, t)) -> 
+	    match clname with 
+	    | Some (cl, b) -> 
+		let t = 
+		  if b then 
+		    let _k = class_info cl in
+		      CHole (Util.dummy_loc, Some Evd.InternalHole)
+		  else CHole (Util.dummy_loc, None)
+		in t, avoid
+	    | None -> failwith ("new instance: under-applied typeclass"))
+	  cl
       | Explicit -> cl
   in
-  let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
-  let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
-  let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in
-  on_free_vars (List.rev (gen_ids @ fvs));
-  let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
-  let ctx, avoid = Classes.name_typeclass_binders bound ctx in
-  let ctx = List.append ctx (List.rev gen_ctx) in
+  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
     let ctx, c = Sign.decompose_prod_assum c' in
-    let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, (List.rev (Array.to_list args))
+    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
+      cl, ctx, imps, (List.rev args)
   in
   let id = 
     match snd instid with
-	Name id -> 
-	  let sp = Lib.make_path id in
-	    if Nametab.exists_cci sp then
-	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
-	    id
-      | Anonymous -> 
-	  let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
-	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
+    | Name id -> 
+	let sp = Lib.make_path id in
+	  if Nametab.exists_cci sp then
+	    errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+	  id
+    | Anonymous -> 
+	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
+	  Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
   let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
-  let substctx = List.map (Evarutil.nf_evar sigma) subst in
-  let subst, _propsctx = 
+  let subst = List.map (Evarutil.nf_evar sigma) subst in
+  let subst = 
     let props = 
-      List.map (fun (x, l, d) -> 
-	x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
-	props
+      match props with
+      | CRecord (loc, _, fs) -> 
+	  if List.length fs > List.length k.cl_props then 
+	    Classes.mismatched_props env' (List.map snd fs) k.cl_props;
+	  fs
+      | _ -> 
+	  if List.length k.cl_props <> 1 then 
+	    errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
+	  else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
     in
-      if List.length props > List.length k.cl_props then 
-	Classes.mismatched_props env' (List.map snd props) k.cl_props;
-      let props, rest = 
-	List.fold_left
-	  (fun (props, rest) (id,_,_) -> 
-	    try 
-	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
-		c :: props, rest'
-	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
-	  ([], props) k.cl_props
-      in
-	if rest <> [] then 
-	  unbound_method env' k.cl_impl (fst (List.hd rest))
-	else
-	  type_ctx_instance isevars env' k.cl_props props substctx
+      match k.cl_props with 
+      | [(na,b,ty)] -> 
+	  let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
+	  let ty' = substl subst ty in
+	  let c = interp_casted_constr_evars isevars env' term ty' in
+	    c :: subst
+      | _ ->
+	  let props, rest = 
+	    List.fold_left
+	      (fun (props, rest) (id,_,_) -> 
+		try 
+		  let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+		  let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
+		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+		    c :: props, rest'
+		with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+	      ([], props) k.cl_props
+	  in
+	    if rest <> [] then 
+	      unbound_method env' k.cl_impl (fst (List.hd rest))
+	    else
+	      fst (type_ctx_instance isevars env' k.cl_props props subst)
+  in
+  let subst = List.fold_left2 
+    (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+    [] subst (k.cl_props @ snd k.cl_context)
   in
-  let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
-    isevars := Evarutil.nf_evar_defs !isevars;
-    let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
-    and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
+  let inst_constr, ty_constr = instance_constructor k subst in
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+  and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
+  in
+    isevars := undefined_evars !isevars;
+    Evarutil.check_evars env Evd.empty !isevars termtype;
+    let hook gr = 
+      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+      let inst = Typeclasses.new_instance k pri global cst in
+	Impargs.declare_manual_implicits false gr ~enriching:false imps;
+	Typeclasses.add_instance inst
     in
-      isevars := undefined_evars !isevars;
-      Evarutil.check_evars env Evd.empty !isevars termtype;
-      let hook gr = 
-	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-	let inst = Typeclasses.new_instance k pri global cst in
-	  Impargs.declare_manual_implicits false gr false imps;
-	  Typeclasses.add_instance inst
-      in
-      let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
-      let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
-	ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls);
-	id
+    let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+    let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+      id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
+	
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index afb0d38d..96a51027 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: subtac_classes.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -34,9 +34,9 @@ val type_ctx_instance :     Evd.evar_defs ref ->
 
 val new_instance : 
   ?global:bool ->
-  Topconstr.local_binder list ->
+  local_binder list ->
   typeclass_constraint ->
-  binder_def_list ->
-  ?on_free_vars:(identifier list -> unit) ->
+  constr_expr ->
+  ?generalize:bool ->
   int option ->
-  identifier
+  identifier * Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4d8f868f..1bbbfbb1 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id: subtac_coercion.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 open Util
 open Names
@@ -33,37 +33,36 @@ open Pp
 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_ = Lazy.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 (Lazy.force sig_).intro
+	then Some (l.(0), l.(1), l.(2), l.(3))
+	else None
+      | _ -> None)
+  | _ -> None
+      
 module Coercion = struct
-
+    
   exception NoSubtacCoercion
-
-  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_ = Lazy.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 (Lazy.force sig_).intro
-		 then Some (l.(0), l.(1), l.(2), l.(3))
-		 else None
-	     | _ -> None)
-      | _ -> None
-
-
+    
   let disc_proj_exist env x =
     match kind_of_term x with
       | App (c, l) ->
diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli
index 53a8d213..5678c10e 100644
--- a/contrib/subtac/subtac_coercion.mli
+++ b/contrib/subtac/subtac_coercion.mli
@@ -1 +1,4 @@
+open Term
+val disc_subset : types -> (types * types) option
+
 module Coercion : Coercion.S
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index a2f54b02..4876b065 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -99,7 +99,7 @@ let interp_binder sigma env na t =
     SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
 
 let interp_context_evars evdref env params = 
-  let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+  let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc ~opaque:false env isevars wf_proof ;
+		    make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
 		    lift lift_cst prop ;
 		    lift lift_cst intern_body_lam |])
       | Some f ->
@@ -385,7 +385,7 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in
+  let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index a393e2c9..cc1e2dde 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,7 +1,9 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 open Printf
 open Pp
 open Subtac_utils
 open Command
+open Environ
 
 open Term
 open Names
@@ -13,9 +15,11 @@ open Decl_kinds
 open Util
 open Evd
 open Declare
+open Proof_type
 
 type definition_hook = global_reference -> unit
 
+let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
@@ -25,15 +29,17 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
-
+type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
+			 * Tacexpr.raw_tactic_expr option) array
+  
 type obligation =
     { obl_name : identifier;
       obl_type : types;
       obl_location : loc;
       obl_body : constr option;
-      obl_opaque : bool;
+      obl_status : obligation_definition_status;
       obl_deps : Intset.t;
+      obl_tac : Tacexpr.raw_tactic_expr option;
     }
 
 type obligations = (obligation array * int)
@@ -79,22 +85,29 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let subst_deps obls deps t =
-  Intset.fold
-    (fun x acc ->
-       let xobl = obls.(x) in
-	 debug 3 (str "Trying to get body of obligation " ++ int x);
-       let oblb = 
-	 try Option.get xobl.obl_body
-	 with _ ->
-	   debug 3 (str "Couldn't get body of obligation " ++ int x);
-	   assert(false)
-       in
-	 Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
-    deps t
-
+let get_obligation_body expand obl =
+  let c = Option.get obl.obl_body in
+    if expand && obl.obl_status = Expand then 
+      match kind_of_term c with
+      | Const c -> constant_value (Global.env ()) c
+      | _ -> c
+    else c
+
+let subst_deps expand obls deps t =
+  let subst =
+    Intset.fold
+      (fun x acc ->
+	let xobl = obls.(x) in
+	let oblb = 
+	  try get_obligation_body expand xobl
+	  with _ -> assert(false)
+	in (xobl.obl_name, oblb) :: acc)
+      deps []
+  in(*  Termops.it_mkNamedProd_or_LetIn t subst *)
+    Term.replace_vars subst t
+    
 let subst_deps_obl obls obl =
-  let t' = subst_deps obls obl.obl_deps obl.obl_type in
+  let t' = subst_deps false obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
 module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -150,14 +163,14 @@ let rec intset_to = function
     -1 -> Intset.empty
   | n -> Intset.add n (intset_to (pred n))
   
-let subst_body prg = 
+let subst_body expand prg = 
   let obls, _ = prg.prg_obligations in
   let ints = intset_to (pred (Array.length obls)) in
-    subst_deps obls ints prg.prg_body,
-  subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+    subst_deps expand obls ints prg.prg_body,
+  subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
     
 let declare_definition prg =
-  let body, typ = subst_body prg in
+  let body, typ = subst_body false prg in
     (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
 		  my_print_constr (Global.env()) body ++ str " : " ++ 
 		  my_print_constr (Global.env()) prg.prg_type);
@@ -188,7 +201,7 @@ let declare_definition prg =
 	in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
-	    Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
+	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
 	  print_message (Subtac_utils.definition_message prg.prg_name);
 	  prg.prg_hook gr;
 	  gr
@@ -216,14 +229,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
 	list_map_i (fun i _ -> i) 0 ctx
 
+let reduce_fix =
+  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
 let declare_mutual_definition l =
   let len = List.length l in
   let fixdefs, fixtypes, fiximps = 
     list_split3
       (List.map (fun x -> 
-	let subs, typ = (subst_body x) in
+	let subs, typ = (subst_body false x) in
 	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
+(*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixkind = Option.get (List.hd l).prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
@@ -248,41 +265,33 @@ let declare_mutual_definition l =
     (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
       
 let declare_obligation obl body =
-  let ce = 
-    { const_entry_body = body;
-      const_entry_type = Some obl.obl_type;
-      const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque;
-      const_entry_boxed = false} 
-  in
-  let constant = Declare.declare_constant obl.obl_name 
-    (DefinitionEntry ce,IsProof Property)
-  in
-    print_message (Subtac_utils.definition_message obl.obl_name);
-    { obl with obl_body = Some (mkConst constant) }
-      
-let try_tactics obls = 
-  Array.map
-    (fun obl ->
-       match obl.obl_body with
-	   None ->
-	     (try
-		let ev = evar_of_obligation obl in
-		let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in	       
-		  declare_obligation obl c		  
-	      with _ -> obl)
-	 | _ -> obl)
-    obls
-        
+  match obl.obl_status with
+  | Expand -> { obl with obl_body = Some body }
+  | Define opaque ->
+      let ce = 
+	{ const_entry_body = body;
+	  const_entry_type = Some obl.obl_type;
+	  const_entry_opaque = 
+	    (if get_proofs_transparency () then false 
+	      else opaque) ;
+	  const_entry_boxed = false} 
+      in
+      let constant = Declare.declare_constant obl.obl_name 
+	(DefinitionEntry ce,IsProof Property)
+      in
+	print_message (Subtac_utils.definition_message obl.obl_name);
+	{ obl with obl_body = Some (mkConst constant) }
+	  
 let red = Reductionops.nf_betaiota
 
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
     Array.mapi
-      (fun i (n, t, l, o, d) ->
+      (fun i (n, t, l, o, d, tac) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; 
-	   obl_location = l; obl_type = red t; obl_opaque = o;
-	   obl_deps = d })
+	   obl_location = l; obl_type = red t; obl_status = o;
+	   obl_deps = d; obl_tac = tac })
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
@@ -369,22 +378,16 @@ let has_dependencies obls n =
     !res
       
 let kind_of_opacity o =
-  if o then Subtac_utils.goal_proof_kind
-  else Subtac_utils.goal_kind
-   
-let obligations_of_evars evars =
-  let arr = 
-    Array.of_list
-      (List.map
-	 (fun (n, t) ->
-	    { obl_name = n;
-	      obl_type = t;
-	      obl_location = dummy_loc;
-	      obl_body = None;
-	      obl_opaque = false;
-	      obl_deps = Intset.empty;
-	    }) evars)
-  in arr, Array.length arr
+  match o with
+  | Define false | Expand -> Subtac_utils.goal_kind
+  | _ -> Subtac_utils.goal_proof_kind
+
+let not_transp_msg = 
+  str "Obligation should be transparent but was declared opaque." ++ spc () ++
+    str"Use 'Defined' instead."
+
+let warn_not_transp () = ppwarn not_transp_msg
+let error_not_transp () = pperror not_transp_msg
 
 let rec solve_obligation prg num =
   let user_num = succ num in
@@ -394,26 +397,37 @@ let rec solve_obligation prg num =
       pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")    
     else
       match deps_remaining obls obl.obl_deps with
-	  [] ->
-	    let obl = subst_deps_obl obls obl in
-	      Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
-		(fun strength gr -> 
-		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
-		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
-		   let obls = Array.copy obls in
-		   let _ = obls.(num) <- obl in
-		     match update_obls prg obls (pred rem) with
-		     | Remain n when n > 0 ->
-			 if has_dependencies obls num then
-			   ignore(auto_solve_obligations (Some prg.prg_name))
-		     | _ -> ());
-	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
-	      Pfedit.by !default_tactic;
-	      Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-
+      | [] ->
+	  let obl = subst_deps_obl obls obl in
+	    Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+	      (fun strength gr -> 
+		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+		let obl = 
+		  let transparent = evaluable_constant cst (Global.env ()) in
+		  let body =
+		    match obl.obl_status with
+		    | Expand ->
+			if not transparent then error_not_transp ()
+			else constant_value (Global.env ()) cst
+		    | Define opaque ->
+			if not opaque && not transparent then error_not_transp ()
+			else Libnames.constr_of_global gr
+		  in { obl with obl_body = Some body }
+		in
+		let obls = Array.copy obls in
+		let _ = obls.(num) <- obl in
+		  match update_obls prg obls (pred rem) with
+		  | Remain n when n > 0 ->
+		      if has_dependencies obls num then
+			ignore(auto_solve_obligations (Some prg.prg_name) None)
+		  | _ -> ());
+	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
+		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+	    Pfedit.by !default_tactic;
+	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+		       ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+	  
 and subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
   let prg = get_prog_err name in
@@ -434,12 +448,17 @@ and solve_obligation_by_tac prg obls i tac =
 	(try
 	    if deps_remaining obls obl.obl_deps = [] then
 	     let obl = subst_deps_obl obls obl in
+	     let tac = 
+	       match tac with
+	       | Some t -> t
+	       | None -> 
+		   match obl.obl_tac with
+		   | Some t -> Tacinterp.interp t
+		   | None -> !default_tactic
+	     in
 	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	       if obl.obl_opaque then 
-		 obls.(i) <- declare_obligation obl t
-	       else
-		 obls.(i) <- { obl with obl_body = Some t };
-	       true		 
+	       obls.(i) <- declare_obligation obl t;
+	       true
 	    else false
 	  with
 	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
@@ -473,34 +492,40 @@ and try_solve_obligation n prg tac =
   let obls' = Array.copy obls in
     if solve_obligation_by_tac prg obls' n tac then
       ignore(update_obls prg obls' (pred rem));
-    
+
 and try_solve_obligations n tac = 
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
-and auto_solve_obligations n : progress =
+and auto_solve_obligations n tac : progress =
   Flags.if_verbose msgnl (str "Solving obligations automatically...");
-  try solve_obligations n !default_tactic with NoObligations _ -> Dependent
+  try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
       
 open Pp
 let show_obligations ?(msg=true) n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
+  let showed = ref 5 in
     if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x -> 
 		   match x.obl_body with 
-		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
-					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
-		    | Some _ -> ())
+		   | None -> 
+		       if !showed > 0 then (
+			 decr showed;
+			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+				   hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
+		   | Some _ -> ())
       obls
-
+      
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
-    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
+	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
@@ -513,12 +538,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=
     let len = Array.length obls in
     let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      let res = auto_solve_obligations (Some n) in
+      let res = auto_solve_obligations (Some n) tactic in
 	match res with
-	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
-	  | _ -> res)
+	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+	| _ -> res)
 	
-let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
@@ -531,8 +556,9 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
       List.fold_left (fun finished x -> 
 	if finished then finished 
 	else
-	  match auto_solve_obligations (Some x) with
-	      Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+	  let res = auto_solve_obligations (Some x) tactic in
+	    match res with
+	    | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
 	    | _ -> false) 
 	false deps
     in ()
@@ -562,8 +588,8 @@ let next_obligation n =
   let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
   let i = 
-    array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
-      obls
+    try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
+    with Not_found -> anomaly "Could not find a solvable obligation."
   in solve_obligation prg i
       			
 let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 6d13e3bd..60c0a413 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,9 +1,14 @@
 open Names
 open Util
 open Libnames
+open Evd
+open Proof_type
 
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
-    (* ident, type, location, opaque or transparent, dependencies *)
+type obligation_info = 
+  (identifier * Term.types * loc * 
+      obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
+    (* ident, type, location, (opaque or transparent, expand or define),
+       dependencies, tactic to solve it *)
 
 type progress = (* Resolution status of a program *)
     | Remain of int  (* n obligations remaining *)
@@ -21,6 +26,7 @@ type definition_hook = global_reference -> unit
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
+  ?tactic:Proof_type.tactic ->
   ?hook:definition_hook -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -28,6 +34,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option)
 val add_mutual_definitions : 
   (Names.identifier * Term.constr * Term.types *
       (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
+  ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   notations ->
   Command.fixpoint_kind -> unit
@@ -36,14 +43,14 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress
+val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
 
-val solve_all_obligations : Proof_type.tactic -> unit 
+val solve_all_obligations : Proof_type.tactic option -> unit 
 
-val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit
+val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
 
-val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit
 
 val show_obligations : ?msg:bool -> Names.identifier option -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index ad76bdeb..07a75720 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *)
 
 open Global
 open Pp
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 559b6ac1..00d37f35 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 open Pp
 open Util
@@ -276,14 +276,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
     | RApp (loc,f,args) -> 
 	let length = List.length args in 
-	let ftycon = 
-	  if length > 0 then
-	    match tycon with
-	    | None -> None
-	    | Some (None, ty) -> mk_abstr_tycon length ty
-	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, length + cur), ty)
-	  else tycon
+	let ftycon =
+	  let ty = 
+	    if length > 0 then
+	      match tycon with
+	      | None -> None
+	      | Some (None, ty) -> mk_abstr_tycon length ty
+	      | Some (Some (init, cur), ty) ->
+		  Some (Some (length + init, length + cur), ty)
+ 	    else tycon
+	  in 
+	    match ty with
+	    | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
+	    | _ -> None
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index bae2731a..cdbc4023 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -159,7 +159,7 @@ let app_opt c e =
 let print_args env args = 
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
-let make_existential loc ?(opaque = true) env isevars c =
+let make_existential loc ?(opaque = Define true) env isevars c =
   let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
   let (key, args) = destEvar evar in
     (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
@@ -232,7 +232,7 @@ let build_dependent_sum l =
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
 	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
 	   with _ -> ());
-	let tac = assert_tac true (Name n) hyptype in
+	let tac = assert_tac (Name n) hyptype in
 	let conttac = 
 	  (fun cont -> 
 	     conttac
@@ -369,7 +369,7 @@ let solve_by_tac evi t =
     Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
     Pfedit.by (tclCOMPLETE t);
-    let _,(const,_,_) = Pfedit.cook_proof ignore in
+    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
   with e ->
     Pfedit.delete_current_proof();
@@ -470,4 +470,3 @@ let tactics_tac s =
 
 let tactics_call tac args =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
-
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 49335211..964f668f 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -83,7 +83,8 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:obligation_definition_status -> 
+  env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
 val evars_of_term : evar_map -> evar_map -> constr -> evar_map