Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 418 insertions, 392 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 465d1d80..42df244d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -19,7 +17,6 @@ open Termops
 open Sign
 open Reduction
 open Proof_type
-open Proof_trees
 open Declarations
 open Tacticals
 open Tacmach
@@ -28,7 +25,7 @@ open Tactics
 open Pattern
 open Clenv
 open Auto
-open Rawterm
+open Glob_term
 open Hiddentac
 open Typeclasses
 open Typeclasses_errors
@@ -38,77 +35,57 @@ open Pfedit
 open Command
 open Libnames
 open Evd
+open Compat
 
-let default_eauto_depth = 100
 let typeclasses_db = "typeclass_instances"
+let typeclasses_debug = ref false
+let typeclasses_depth = ref None
 
-let _ = Auto.auto_init := (fun () ->
-  Auto.create_hint_db false typeclasses_db full_transparent_state true)
+let _ = 
+  Auto.add_auto_init 
+    (fun () -> Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
 exception Found of evar_map
 
-let is_dependent ev evm =
-  Evd.fold (fun ev' evi dep ->
-    if ev = ev' then dep
-    else dep || occur_evar ev evi.evar_concl)
-    evm false
-
-let valid goals p res_sigma l =
-  let evm =
-    List.fold_left2
-      (fun sigma (ev, evi) prf ->
-	let cstr, obls = Refiner.extract_open_proof !res_sigma prf in
-	  if not (Evd.is_defined sigma ev) then
-	    Evd.define ev cstr sigma
-	  else sigma)
-      !res_sigma goals l
-  in raise (Found evm)
-
-let evar_filter evi =
-  let hyps' = evar_filtered_context evi in
-    { evi with 
-      evar_hyps = Environ.val_of_named_context hyps';
-      evar_filter = List.map (fun _ -> true) hyps' }
+(** We transform the evars that are concerned by this resolution
+    (according to predicate p) into goals.
+    Invariant: function p only manipulates undefined evars *)
 
 let evars_to_goals p evm =
   let goals, evm' =
-    Evd.fold
+    Evd.fold_undefined
       (fun ev evi (gls, evm') ->
-	if evi.evar_body = Evar_empty then
-	  let evi', goal = p evm ev evi in
-	    if goal then
-	      ((ev, evi') :: gls, Evd.add evm' ev evi')
-	    else (gls, Evd.add evm' ev evi')
-	else (gls, Evd.add evm' ev evi))
-      evm ([], Evd.empty)
+	let evi', goal = p evm ev evi in
+	let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in
+	(gls', Evd.add evm' ev evi'))
+      evm ([], Evd.defined_evars evm)
   in
-    if goals = [] then None
-    else
-      let goals = List.rev goals in
-      let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in
-	Some (goals, evm')
+  if goals = [] then None else Some (List.rev goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
 
-let intersects s t =
-  Intset.exists (fun el -> Intset.mem el t) s
-
 open Auto
 
 let e_give_exact flags c gl = 
   let t1 = (pf_type_of gl c) in
     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
 
-let assumption flags id = e_give_exact flags (mkVar id)
-
 open Unification
 
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = var_full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = false;
   resolve_evars = false;
-  use_evars_pattern_unification = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = true;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
 }
 
 let rec eq_constr_mod_evars x y =
@@ -126,18 +103,18 @@ let progress_evars t gl =
   in tclTHEN t check gl
 
 TACTIC EXTEND progress_evars
-  [ "progress_evars" tactic(t) ] -> [ progress_evars (snd t) ]
+  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ]
 END
 
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    tclPROGRESS (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
 
 let unify_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv' gls
 
 let clenv_of_prods nprods (c, clenv) gls =
   if nprods = 0 then Some clenv
@@ -157,7 +134,9 @@ let with_prods nprods (c, clenv) f gls =
 
 let flags_of_state st =
   {auto_unif_flags with
-    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st; 
+     modulo_delta_types = st;
+     modulo_eta = false}
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
@@ -168,11 +147,11 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
 	      (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map (fun (x,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+    (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
-and e_my_find_search db_list local_db hdc concl =
+and e_my_find_search db_list local_db hdc complete concl =
   let hdc = head_of_constr_reference hdc in
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
@@ -188,7 +167,7 @@ and e_my_find_search db_list local_db hdc concl =
       (local_db::db_list)
   in
   let tac_of_hint =
-    fun (flags, {pri=b; pat = p; code=t}) ->
+    fun (flags, {pri = b; pat = p; code = t; name = name}) ->
       let tac =
 	match t with
 	  | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve flags)
@@ -196,66 +175,55 @@ and e_my_find_search db_list local_db hdc concl =
 	  | Give_exact (c) -> e_give_exact flags c
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags))
-		(e_trivial_fail_db db_list local_db)
+	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
-	  | Extern tacast -> conclPattern concl p tacast
+	  | Extern tacast -> 
+(* 	    tclTHEN *)
+(* 	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *)
+	      (conclPattern concl p tacast)
       in
+      let tac = if complete then tclCOMPLETE tac else tac in
 	match t with
-	| Extern _ -> (tac,b,true,lazy (pr_autotactic t))
-	| _ -> (tac,b,false,lazy (pr_autotactic t))
+	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	| _ -> 
+(* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
+	    (tac,b,false, name, lazy (pr_autotactic t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
   try
     e_my_find_search db_list local_db
-      (fst (head_constr_bound gl)) gl
+    (fst (head_constr_bound gl)) true gl
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
   try
     e_my_find_search db_list local_db
-      (fst (head_constr_bound gl)) gl
+      (fst (head_constr_bound gl)) false gl
   with Bound | Not_found -> []
 
 let rec catchable = function
   | Refiner.FailError _ -> true
-  | Stdpp.Exc_located (_, e) -> catchable e
+  | Loc.Exc_located (_, e) -> catchable e
   | e -> Logic.catchable_exception e
 
-let is_dep gl gls =
-  let evs = Evarutil.evars_of_term gl.evar_concl in
-    if evs = Intset.empty then false
-    else
-      List.fold_left
-	(fun b gl ->
-	  if b then b
-	  else
-	    let evs' = Evarutil.evars_of_term gl.evar_concl in
-	      intersects evs evs')
-	false gls
-
-let is_ground gl =
-  Evarutil.is_ground_term (project gl) (pf_concl gl)
-
 let nb_empty_evars s =
-  Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
+  Evd.fold_undefined (fun ev evi acc -> succ acc) s 0
 
-let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
-
-let typeclasses_debug = ref false
-
-type validation = evar_map -> proof_tree list -> proof_tree
+let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
 let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
 
 type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
-		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t}
+		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
+		  auto_path : global_reference option list;
+		  auto_cut : hints_path }
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
 type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
 
-type auto_result = autogoal list sigma * validation
+type auto_result = autogoal list sigma
 
 type atac = auto_result tac
 
@@ -272,26 +240,67 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	       if not (eq_constr ty' ar) then iscl env' ty'
 	       else false
   in
-  let keep = not only_classes || iscl env cty in
-    if keep then let c = mkVar id in
-      map_succeed 
-	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
-	[make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
+  let is_class = iscl env cty in
+  let keep = not only_classes || is_class in
+    if keep then 
+      let c = mkVar id in
+      let name = PathHints [VarRef id] in
+      let hints =
+	if is_class then
+	  let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+	    (list_map_append
+	       (fun (pri, c) -> make_resolves env sigma 
+		  (true,false,Flags.is_verbose()) pri c) 
+	       hints)
+	else []
+      in
+        (hints @ map_succeed 
+	 (fun f -> try f (c,cty) with UserError _ -> failwith "") 
+	 [make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri])
     else []
 
 let pf_filtered_hyps gls = 
-  evar_filtered_context (sig_it gls)
+  Goal.V82.hyps gls.Evd.sigma (sig_it gls)
+
+let make_hints g st only_classes sign =
+  let paths, hintlist = 
+    List.fold_left 
+    (fun (paths, hints) hyp ->
+     if is_section_variable (pi1 hyp) then (paths, hints)
+     else
+       let path, hint = 		    
+	 PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+       in
+	 (PathOr (paths, path), hint @ hints))
+    (PathEmpty, []) sign
+  in Hint_db.add_list hintlist (Hint_db.empty st true)
+
+let autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None
+let freeze () = !autogoal_hints_cache
+let unfreeze v = autogoal_hints_cache := v
+let init () = autogoal_hints_cache := None
+
+let _ = init ()
 
-let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
-  let sign = pf_filtered_hyps g in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in
-    Hint_db.add_list hintlist (Hint_db.empty st true)
-  
+let _ =
+  Summary.declare_summary "autogoal-hints-cache"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+    
+let make_autogoal_hints = 
+  fun only_classes ?(st=full_transparent_state) g ->
+    let sign = pf_filtered_hyps g in
+      match freeze () with
+      | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints
+      | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
+	  unfreeze (Some (sign, hints)); hints
+	  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->
     let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
       match res with
-      | Some (gls,v) -> sk (f gls hints, fun _ -> v) fk
+      | Some gls -> sk (f gls hints) fk
       | None -> fk () }
 
 let intro_tac : atac =
@@ -299,28 +308,22 @@ let intro_tac : atac =
     (fun {it = gls; sigma = s} info ->
       let gls' =
 	List.map (fun g' ->
-	  let env = evar_env g' in
+	  let env = Goal.V82.env s g' in
+	  let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
 	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) 
-	    (true,false,false) info.only_classes None (List.hd (evar_context g')) in
+	    (true,false,false) info.only_classes None (List.hd context) in
 	  let ldb = Hint_db.add_list hint info.hints in
 	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
       in {it = gls'; sigma = s})
 
 let normevars_tac : atac = 
-  lift_tactic tclNORMEVAR
-    (fun {it = gls; sigma = s} info ->
-      let gls' =
-	List.map (fun g' ->
-	  (g', { info with auto_last_tac = lazy (str"NORMEVAR") })) gls
-      in {it = gls'; sigma = s})
-
-
-let id_tac : atac =
-  { skft = fun sk fk {it = gl; sigma = s} ->
-    sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk }
+  { skft = fun sk fk {it = (gl, info); sigma = s} ->
+    let gl', sigma' = Goal.V82.nf_evar s gl in
+    let info' = { info with auto_last_tac = lazy (str"normevars") } in
+      sk {it = [gl', info']; sigma = sigma'} fk }
 
 (* Ordering of states is lexicographic on the number of remaining goals. *)
-let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) =
+let compare (pri, _, _, res) (pri', _, _, res') =
   let nbgoals s =
     List.length (sig_it s) + nb_empty_evars (sig_sig s)
   in
@@ -331,131 +334,104 @@ let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) =
 let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
-let solve_tac (x : 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> 
-    if gls = [] then sk res fk else fk ()) fk gls }
-
-let solve_unif_tac : atac =
-  { skft = fun sk fk {it = gl; sigma = s} -> 
-    try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in
-	  normevars_tac.skft sk fk ({it=gl; sigma=s'})
-    with _ -> fk () }
-
 let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s} ->
-    let possible_resolve ((lgls,v) as res, pri, b, pp) =
-      (pri, pp, b, res)
-    in
-    let tacs =
-      let concl = gl.evar_concl in
+      let concl = Goal.V82.concl s gl in
+      let tacgl = {it = gl; sigma = s} in
       let poss = e_possible_resolve hints info.hints concl in
-      let l =
-	let tacgl = {it = gl; sigma = s} in
-	Util.list_map_append (fun (tac, pri, b, pptac) ->
-	  try [tac tacgl, pri, b, pptac] with e when catchable e -> [])
-	  poss
-      in
-	if l = [] && !typeclasses_debug then
-	  msgnl (pr_depth info.auto_depth ++ str": no match for " ++
-		    Printer.pr_constr_env (Evd.evar_env gl) concl ++
-		    spc () ++ int (List.length poss) ++ str" possibilities");
-	List.map possible_resolve l
-    in
-    let tacs = List.sort compare tacs in
-    let rec aux i = function
-      | (_, pp, b, ({it = gls; sigma = s}, v)) :: tl ->
-	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
-					       ++ str" on" ++ spc () ++ pr_ev s gl);
-	  let fk =
-	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
-	    aux (succ i) tl)
+      let rec aux i foundone = function
+	| (tac, _, b, name, pp) :: tl ->
+	  let derivs = path_derivate info.auto_cut name in
+	  let res = 
+            try
+		if path_matches derivs [] then None else Some (tac tacgl)
+	    with e when catchable e -> None 
 	  in
-	  let sgls = evars_to_goals (fun evm ev evi ->
-	    if Typeclasses.is_resolvable evi && 
-	      (not info.only_classes || Typeclasses.is_class_evar evm evi) then
-	      Typeclasses.mark_unresolvable evi, true
-	    else evi, false) s
-	  in
-	  let nbgls, newgls, s' =
-	    let gls' = List.map (fun g -> (None, g)) gls in
-	    match sgls with
-	    | None -> List.length gls', gls', s
-	    | Some (evgls, s') ->
-		(List.length gls', gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s')
-	  in
-	  let gls' = list_map_i (fun j (evar, g) -> 
-	    let info = 
-	      { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
-		is_evar = evar;
-		hints = 
-		  if b && g.evar_hyps <> gl.evar_hyps 
-		  then make_autogoal_hints info.only_classes
-		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
-		  else info.hints }
-	    in g, info) 1 newgls in
-	  let glsv = {it = gls'; sigma = s'}, (fun _ pfl -> v (list_firstn nbgls pfl)) in
-	    sk glsv fk
-      | [] -> fk ()
-    in aux 1 tacs }
-
-let evars_of_term c =
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) -> Intset.add n acc
-    | _ -> fold_constr evrec acc c
-  in evrec Intset.empty c
-
-exception Found_evar of int
-
-let occur_evars evars c =
-  try
-    let rec evrec c =
-      match kind_of_term c with
-      | Evar (n, _) -> if Intset.mem n evars then raise (Found_evar n) else ()
-      | _ -> iter_constr evrec c
-    in evrec c; false
-  with Found_evar _ -> true
-
-let dependent only_classes evd oev concl =
-  let concl_evars = Intset.union (evars_of_term concl)
-    (Option.cata Intset.singleton Intset.empty oev)
-  in not (Intset.is_empty concl_evars) 
+	    (match res with
+	       | None -> aux i foundone tl
+	       | Some {it = gls; sigma = s'} ->
+	    	   if !typeclasses_debug then
+		     msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+			    ++ str" on" ++ spc () ++ pr_ev s gl);
+		   let fk =
+		     (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ Lazy.force pp);
+			aux (succ i) true tl)
+		   in
+		   let sgls =
+		     evars_to_goals
+		       (fun evm ev evi ->
+			  if Typeclasses.is_resolvable evi &&
+			    (not info.only_classes || Typeclasses.is_class_evar evm evi)
+			  then Typeclasses.mark_unresolvable evi, true
+			  else evi, false) s'
+		   in
+		   let newgls, s' =
+		     let gls' = List.map (fun g -> (None, g)) gls in
+		       match sgls with
+		       | None -> gls', s'
+		       | Some (evgls, s') ->
+			 (* Reorder with dependent subgoals. *)
+			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
+		   in
+		   let gls' = list_map_i
+		     (fun j (evar, g) ->
+			let info =
+			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+			      is_evar = evar;
+			      hints =
+			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
+			      then make_autogoal_hints info.only_classes
+				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
+			      else info.hints;
+			      auto_cut = derivs }
+			in g, info) 1 newgls in
+		   let glsv = {it = gls'; sigma = s'} in
+		     sk glsv fk)
+	| [] ->
+	  if not foundone && !typeclasses_debug then
+	    msgnl (pr_depth info.auto_depth ++ str": no match for " ++
+		     Printer.pr_constr_env (Goal.V82.env s gl) concl ++
+		     spc () ++ int (List.length poss) ++ str" possibilities");
+	  fk ()
+    in aux 1 false poss }
+
+let isProp env sigma concl = 
+  let ty = Retyping.get_type_of env sigma concl in
+    kind_of_term ty = Sort (Prop Null)
+
+let needs_backtrack only_classes env evd oev concl =
+  if oev = None || isProp env evd concl then
+    not (Intset.is_empty (Evarutil.evars_of_term concl))
+  else true
 
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
-  let rec aux s (acc : (autogoal list * validation) list) fk = function
+  let rec aux s (acc : autogoal list list) fk = function
     | (gl,info) :: gls ->
-	second.skft (fun ({it=gls';sigma=s'},v') fk' ->
-	  let s', needs_backtrack = 
-	    if gls' = [] then
-	      match info.is_evar with
-	      | Some ev -> 
-		  let s' = 
-		    if Evd.is_defined s' ev then s' 
-		    else
-		      let prf = v' s' [] in
-		      let term, _ = Refiner.extract_open_proof s' prf in
-			Evd.define ev term s' 
-		  in s', dependent info.only_classes s' (Some ev) gl.evar_concl
-	      | None -> s', dependent info.only_classes s' None gl.evar_concl
-	    else s', true
-	  in
-	  let fk'' = if not needs_backtrack then
-	    (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' 
-	  in aux s' ((gls',v')::acc) fk'' gls)
-	  fk {it = (gl,info); sigma = s}
+	(match info.is_evar with 
+	 | Some ev when Evd.is_defined s ev -> aux s acc fk gls
+	 | _ -> 
+	     second.skft
+	       (fun {it=gls';sigma=s'} fk' ->
+		  let needs_backtrack = 
+		    if gls' = [] then
+ 		      needs_backtrack info.only_classes
+		        (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
+		    else true
+		  in
+		  let fk'' = 
+		    if not needs_backtrack then
+		      (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl ++ 
+							 str " after " ++ Lazy.force info.auto_last_tac); fk) 
+		    else fk' 
+		  in aux s' (gls'::acc) fk'' gls)
+	       fk {it = (gl,info); sigma = s})
     | [] -> Some (List.rev acc, s, fk)
-  in fun ({it = gls; sigma = s},v) fk ->
+  in fun {it = gls; sigma = s} fk ->
     let rec aux' = function
       | None -> fk ()
       | Some (res, s', fk') ->
-	  let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in
-	  let v' s' pfs' : proof_tree =
-	    let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) ->
-	      let before, after = list_split_at (List.length gls) pfs' in
-		(v s' before :: newpfs, after))
-	      ([], pfs') res
-	    in assert(rest = []); v s' (List.rev newpfs)
-	  in sk ({it = goals'; sigma = s'}, v') (fun () -> aux' (fk' ()))
+	  let goals' = List.concat res in
+	    sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ()))
     in aux' (aux s [] (fun () -> None) gls)
 
 let then_tac (first : atac) (second : atac) : atac =
@@ -468,52 +444,68 @@ type run_list_res = (auto_result * run_list_res fk) option
 
 let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
   (then_list t (fun x fk -> Some (x, fk)))
-    (gl, fun s pfs -> valid goals p (ref s) pfs)
+    gl
     (fun _ -> None)
 
+let fail_tac : atac = 
+  { skft = fun sk fk _ -> fk () }
+
 let rec fix (t : 'a tac) : 'a tac =
   then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
 
-let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g =
+let rec fix_limit limit (t : 'a tac) : 'a tac =
+  if limit = 0 then fail_tac 
+  else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
+    
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
   let hints = make_autogoal_hints only_classes ~st g in
     (g.it, { hints = hints ; is_evar = ev; 
-	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (mt()) })
+	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none");
+	     auto_path = []; auto_cut = cut })
       
-let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
+
+let cut_of_hints h =
+  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+
+let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
+  let cut = cut_of_hints hints in
   { it = list_map_i (fun i g -> 
-    let (gl, auto) = make_autogoal ~only_classes ~st (Some (fst g)) {it = snd g; sigma = evm'} in
+    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
 let get_result r = 
   match r with
   | None -> None
-  | Some ((gls, v), fk) ->
-      try ignore(v (sig_sig gls) []); assert(false)
-      with Found evm' -> Some (evm', fk)
-
-let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
+  | Some (gls, fk) -> Some (gls.sigma,fk)
+	
+let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
   match evars_to_goals p evm with
   | None -> None (* This happens only because there's no evar having p *)
   | Some (goals, evm') ->
-      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
+      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st hints goals evm') in
 	match get_result res with
 	| None -> raise Not_found
-	| Some (evm', fk) -> Some (evars_reset_evd evm' evm, fk)
+	| Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk)
 	    
 let eauto_tac hints = 
-  fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
-  
-let eauto ?(only_classes=true) ?st hints g =
-  let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
-    match run_tac (eauto_tac hints) gl with
+  then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
+
+let eauto_tac ?limit hints = 
+  match limit with
+  | None -> fix (eauto_tac hints)
+  | Some limit -> fix_limit limit (eauto_tac hints)
+      
+let eauto ?(only_classes=true) ?st ?limit hints g =
+  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g } in
+    match run_tac (eauto_tac ?limit hints) gl with
     | None -> raise Not_found
-    | Some ({it = goals; sigma = s}, valid) ->
-	{it = List.map fst goals; sigma = s}, valid s
+    | Some {it = goals; sigma = s} ->
+	{it = List.map fst goals; sigma = s}
 
-let real_eauto st hints p evd =
+let real_eauto st ?limit hints p evd =
   let rec aux evd fails =
     let res, fails =
-      try run_on_evars ~st p evd (eauto_tac hints), fails
+      try run_on_evars ~st p evd hints (eauto_tac ?limit hints), fails
       with Not_found ->
 	List.fold_right (fun fk (res, fails) ->
 	  match res with
@@ -526,162 +518,209 @@ let real_eauto st hints p evd =
       | Some (evd', fk) -> aux evd' (fk :: fails)
   in aux evd []
 
-let resolve_all_evars_once debug (mode, depth) p evd =
+let resolve_all_evars_once debug limit p evd =
   let db = searchtable_map typeclasses_db in
-    real_eauto (Hint_db.transparent_state db) [db] p evd
+    real_eauto ?limit (Hint_db.transparent_state db) [db] p evd
+
+(** We compute dependencies via a union-find algorithm.
+    Beware of the imperative effects on the partition structure,
+    it should not be shared, but only used locally. *)
+
+module Intpart = Unionfind.Make(Intset)(Intmap)
 
-exception FoundTerm of constr
+let deps_of_constraints cstrs evm p =
+  List.iter (fun (_, _, x, y) ->
+    let evx = Evarutil.undefined_evars_of_term evm x in
+    let evy = Evarutil.undefined_evars_of_term evm y in
+    Intpart.union_set (Intset.union evx evy) p)
+    cstrs
+
+let evar_dependencies evm p =
+  Evd.fold_undefined
+    (fun ev evi _ ->
+      let evars = Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+      in Intpart.union_set evars p)
+    evm ()
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
-  let gls = { it = Evd.make_evar (Environ.named_context_val env) gl; sigma = sigma } in
+  let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
+  let (gl,t,sigma) = 
+    Goal.V82.mk_goal sigma nc gl Store.empty in
+  let gls = { it = gl ; sigma = sigma } in
   let hints = searchtable_map typeclasses_db in
-  let gls', v = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
-  let term = v [] in
+  let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
   let evd = sig_sig gls' in
-  let term = fst (Refiner.extract_open_proof evd term) in
-  let term = Evarutil.nf_evar evd term in
+  let t' = let (ev, inst) = destEvar t in
+    mkEvar (ev, Array.of_list subst)
+  in
+  let term = Evarutil.nf_evar evd t' in
     evd, term
 
 let _ =
   Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
 
-let has_undefined p oevd evd =
-  Evd.fold (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && snd (p oevd ev evi)))
-    evd false
-
-let rec merge_deps deps = function
-  | [] -> [deps]
-  | hd :: tl ->
-      if intersects deps hd then
-	merge_deps (Intset.union deps hd) tl
-      else hd :: merge_deps deps tl
-
-let evars_of_evi evi =
-  Intset.union (evars_of_term evi.evar_concl)
-    (Intset.union
-	(match evi.evar_body with
-	| Evar_empty -> Intset.empty
-	| Evar_defined b -> evars_of_term b)
-	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
-
-let deps_of_constraints cstrs deps =
-  List.fold_right (fun (_, _, x, y) deps -> 
-    let evs = Intset.union (evars_of_term x) (evars_of_term y) in
-      merge_deps evs deps)
-    cstrs deps
-      
-let evar_dependencies evm =
-  Evd.fold 
-    (fun ev evi acc ->
-      merge_deps (Intset.union (Intset.singleton ev) 
-		     (evars_of_evi evi)) acc)
-    evm []
+(** [split_evars] returns groups of undefined evars according to dependencies *)
 
 let split_evars evm =
-  let _, cstrs = extract_all_conv_pbs evm in
-  let evmdeps = evar_dependencies evm in
-  let deps = deps_of_constraints cstrs evmdeps in
-    List.sort Intset.compare deps
+  let p = Intpart.create () in
+  evar_dependencies evm p;
+  deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
+  Intpart.partition p
+
+(** [evars_in_comp] filters an [evar_map], keeping only evars
+    that belongs to a certain component *)
 
-let select_evars evs evm =
-  Evd.fold (fun ev evi acc ->
-    if Intset.mem ev evs then Evd.add acc ev evi else acc)
-    evm Evd.empty
+let evars_in_comp comp evm =
+  try
+    evars_reset_evd 
+      (Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
+	 comp Evd.empty) evm
+  with Not_found -> assert false
 
-let is_inference_forced p ev evd =
+let is_inference_forced p evd ev =
   try
-    let evi = Evd.find evd ev in
-      if evi.evar_body = Evar_empty then
-	if Typeclasses.is_resolvable evi
-	  && snd (p ev evi)
-	then
-	  let (loc, k) = evar_source ev evd in
-	    match k with
-	    | ImplicitArg (_, _, b) -> b
-	    | QuestionMark _ -> false
-	    | _ -> true
-	else true
-      else false
-  with Not_found -> true
-
-let is_optional p comp evd =
-  Intset.fold (fun ev acc ->
-    acc && not (is_inference_forced p ev evd))
-    comp true
+    let evi = Evd.find_undefined evd ev in
+    if Typeclasses.is_resolvable evi && snd (p ev evi)
+    then
+      let (loc, k) = evar_source ev evd in
+      match k with
+	| ImplicitArg (_, _, b) -> b
+	| QuestionMark _ -> false
+	| _ -> true
+    else true
+  with Not_found -> assert false
+
+let is_mandatory p comp evd =
+  Intset.exists (is_inference_forced p evd) comp
+
+(** In case of unsatisfiable constraints, build a nice error message *)
+
+let error_unresolvable env comp do_split evd =
+  let evd = Evarutil.nf_evar_map_undefined evd in
+  let evm = if do_split then evars_in_comp comp evd else evd in
+  let _, ev = Evd.fold_undefined
+    (fun ev evi (b,acc) ->
+      (* focus on one instance if only one was searched for *)
+      if class_of_constr evi.evar_concl <> None then
+	if not b (* || do_split *) then
+	  true, Some ev
+	else b, None
+      else b, acc) evm (false, None)
+  in
+  Typeclasses_errors.unsatisfiable_constraints
+    (Evarutil.nf_env_evar evm env) evm ev
+
+(** Check if an evar is concerned by the current resolution attempt,
+    (and in particular is in the current component), and also update
+    its evar_info.
+    Invariant : this should only be applied to undefined evars,
+    and return undefined evar_info *)
+
+let select_and_update_evars p oevd in_comp evd ev evi =
+  assert (evi.evar_body = Evar_empty);
+  try
+    let oevi = Evd.find_undefined oevd ev in
+    if Typeclasses.is_resolvable oevi then
+      Typeclasses.mark_unresolvable evi,
+      (in_comp ev && p evd ev evi)
+    else evi, false
+  with Not_found ->
+    Typeclasses.mark_unresolvable evi, p evd ev evi
+
+(** Do we still have unresolved evars that should be resolved ? *)
+
+let has_undefined p oevd evd =
+  Evd.fold_undefined (fun ev evi has -> has ||
+    snd (p oevd ev evi))
+    evd false
+
+(** If [do_split] is [true], we try to separate the problem in
+    several components and then solve them separately *)
+
+exception Unresolved
 
 let resolve_all_evars debug m env p oevd do_split fail =
   let split = if do_split then split_evars oevd else [Intset.empty] in
-  let p = if do_split then
-    fun comp evd ev evi -> 
-      if evi.evar_body = Evar_empty then
-	(try let oevi = Evd.find oevd ev in
-	       if Typeclasses.is_resolvable oevi then
-		 Typeclasses.mark_unresolvable evi, (Intset.mem ev comp &&
-							p evd ev evi)
-	       else evi, false
-	  with Not_found ->
-	    Typeclasses.mark_unresolvable evi, p evd ev evi)
-      else evi, false
-    else fun _ evd ev evi -> 
-      if evi.evar_body = Evar_empty then
-	try let oevi = Evd.find oevd ev in
-	      if Typeclasses.is_resolvable oevi then
-		Typeclasses.mark_unresolvable evi, p evd ev evi
-	      else evi, false
-	with Not_found ->
-	  Typeclasses.mark_unresolvable evi, p evd ev evi
-      else evi, false
-  in
-  let rec aux p evd =
-    let evd' = resolve_all_evars_once debug m p evd in
-      if has_undefined p oevd evd' then None
-      else Some evd'
+  let in_comp comp ev = if do_split then Intset.mem ev comp else true
   in
   let rec docomp evd = function
     | [] -> evd
     | comp :: comps ->
-	let res = try aux (p comp) evd with Not_found -> None in
-	  match res with
-	  | None -> 
-	      if fail && (not do_split || not (is_optional (p comp evd) comp evd)) then
-		(* Unable to satisfy the constraints. *)		
-		let evd = Evarutil.nf_evars evd in
-		let evm = if do_split then select_evars comp evd else evd in
-		let _, ev = Evd.fold
-		  (fun ev evi (b,acc) ->
-		    (* focus on one instance if only one was searched for *)
-		    if class_of_constr evi.evar_concl <> None then
-		      if not b (* || do_split *) then
-			true, Some ev
-		      else b, None
-		    else b, acc) evm (false, None)
-		in
-		  Typeclasses_errors.unsatisfiable_constraints (Evarutil.nf_env_evar evm env) evm ev
-	      else (* Best effort: do nothing *) oevd
-	  | Some evd' -> docomp evd' comps
+      let p = select_and_update_evars p oevd (in_comp comp) in
+      try
+	 let evd' = resolve_all_evars_once debug m p evd in
+	 if has_undefined p oevd evd' then raise Unresolved;
+	 docomp evd' comps
+      with Unresolved | Not_found ->
+	if fail && (not do_split || is_mandatory (p evd) comp evd)
+	then (* Unable to satisfy the constraints. *)
+	  error_unresolvable env comp do_split evd
+	else (* Best effort: do nothing on this component *) 
+	  docomp evd comps
   in docomp oevd split
 
-let resolve_typeclass_evars d p env evd onlyargs split fail =
-  let pred =
-    if onlyargs then
-      (fun evd ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
-	Typeclasses.is_class_evar evd evi)
-    else (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
-  in resolve_all_evars d p env pred evd split fail
+let initial_select_evars onlyargs =
+  if onlyargs then
+    (fun evd ev evi ->
+      Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd))
+      && Typeclasses.is_class_evar evd evi)
+  else
+    (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
+
+let resolve_typeclass_evars debug m env evd onlyargs split fail =
+  let evd = 
+    try Evarconv.consider_remaining_unif_problems
+      ~ts:(Typeclasses.classes_transparent_state ()) env evd
+    with _ -> evd
+  in
+    resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
 
-let solve_inst debug mode depth env evd onlyargs split fail =
-  resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail
+let solve_inst debug depth env evd onlyargs split fail =
+  resolve_typeclass_evars debug depth env evd onlyargs split fail
 
 let _ =
   Typeclasses.solve_instanciations_problem :=
-    solve_inst false true default_eauto_depth
+    solve_inst false !typeclasses_depth
+
+
+(** Options: depth, debug and transparency settings. *)
+
+open Goptions
+
+let set_typeclasses_debug d = (:=) typeclasses_debug d;
+  Typeclasses.solve_instanciations_problem := solve_inst d !typeclasses_depth
+    
+let get_typeclasses_debug () = !typeclasses_debug
+
+let set_typeclasses_debug =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "debug output for typeclasses proof search";
+      optkey   = ["Typeclasses";"Debug"];
+      optread  = get_typeclasses_debug;
+      optwrite = set_typeclasses_debug; }
+
+
+let set_typeclasses_depth d = (:=) typeclasses_depth d;
+  Typeclasses.solve_instanciations_problem := solve_inst !typeclasses_debug !typeclasses_depth
+    
+let get_typeclasses_depth () = !typeclasses_depth
+
+let set_typeclasses_depth =
+  declare_int_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "depth for typeclasses proof search";
+      optkey   = ["Typeclasses";"Depth"];
+      optread  = get_typeclasses_depth;
+      optwrite = set_typeclasses_depth; }
 
 let set_transparency cl b =
   List.iter (fun r -> 
     let gr = Smartlocate.global_with_alias r in
     let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
-      Classes.set_typeclass_transparency ev b) cl
+      Classes.set_typeclass_transparency ev false b) cl
 
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
@@ -704,18 +743,6 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
-let pr_mode _prc _prlc _prt m =
-  match m with
-      Some b ->
-	if b then Pp.str "depth-first" else Pp.str "breadth-fist"
-    | None -> Pp.mt()
-
-ARGUMENT EXTEND search_mode TYPED AS bool option PRINTED BY pr_mode
-| [ "dfs" ] -> [ Some true ]
-| [ "bfs" ] -> [ Some false ]
-| [] -> [ None ]
-END
-
 let pr_depth _prc _prlc _prt = function
     Some i -> Util.pr_int i
   | None -> Pp.mt()
@@ -724,13 +751,12 @@ ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
 | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
 END
 
+(* true = All transparent, false = Opaque if possible *)
+
 VERNAC COMMAND EXTEND Typeclasses_Settings
- | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [
-     typeclasses_debug := d;
-     let mode = match s with Some t -> t | None -> true in
-     let depth = match depth with Some i -> i | None -> default_eauto_depth in
-       Typeclasses.solve_instanciations_problem :=
-	 solve_inst d mode depth
+ | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+     set_typeclasses_debug d;
+     set_typeclasses_depth depth
    ]
 END
 
@@ -738,8 +764,8 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl
   try 
     let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
     let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
-      eauto ~only_classes ~st dbs gl
-   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl
+      eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
+   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
  
 TACTIC EXTEND typeclasses_eauto
 | [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]