Purely refactoring and code/API cleanup.

Fix test-suite files

7 files changed, 957 insertions, 887 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 845ac6713..cc8fd53a7 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -958,7 +958,6 @@ TACTIC EXTEND revgoals
 | [ "revgoals" ] -> [ Proofview.revgoals ]
 END
 
-
 type cmp =
   | Eq
   | Lt | Le
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 01af90e27..eaa6aad4f 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -16,10 +16,6 @@ open Constrarg
 
 DECLARE PLUGIN "g_class"
 
-TACTIC EXTEND progress_evars
-  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
-END
-
 (** Options: depth, debug and transparency settings. *)
 
 let set_transparency cl b =
@@ -65,10 +61,12 @@ VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
    ]
 END
 
+(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
-| [ "typeclasses" "eauto" ] -> [
-    typeclasses_eauto ~only_classes:true [Hints.typeclasses_db] ]
+ | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+    [ typeclasses_eauto d l ]
+ | [ "typeclasses" "eauto" depth(d) ] -> [
+     typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
 
 TACTIC EXTEND head_of_constr
@@ -87,23 +85,30 @@ TACTIC EXTEND autoapply
   [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
 END
 
-open G_auto
-       
-TACTIC EXTEND fulleauto
-| ["fulleauto" depth(depth) "with" ne_preident_list(dbnames) ] -> [
-    let dbs = match dbnames with [] -> ["typeclass_instances"]
-                               | l -> l in
-    let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth true dbs
-  ]
-| ["fulleauto" depth(depth) ] -> [
-    let dbs = ["typeclass_instances"] in
-    let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth true dbs
-  ]
-| ["fulleauto" ] -> [
-    let dbs = ["typeclass_instances"] in
-    let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false true dbs
-  ]
+(** TODO: DEPRECATE *)
+(* A progress test that allows to see if the evars have changed *)
+open Term
+open Proofview.Goal
+open Proofview.Notations
+
+let rec eq_constr_mod_evars x y =
+  match kind_of_term x, kind_of_term y with
+  | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true
+  | _, _ -> compare_constr eq_constr_mod_evars x y
+
+let progress_evars t =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    let check =
+      Proofview.Goal.nf_enter { enter = begin fun gl' ->
+        let newconcl = Proofview.Goal.concl gl' in
+        if eq_constr_mod_evars concl newconcl
+        then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
+        else Proofview.tclUNIT ()
+      end }
+    in t <*> check
+  end }
+
+TACTIC EXTEND progress_evars
+  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
 END
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 61a8956e0..0ddb97dbb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* TODO: 
+(* TODO:
   - Find an interface allowing eauto to backtrack when shelved goals remain,
-   e.g. to force instantiations. 
+   e.g. to force instantiations.
   - unique solutions
  *)
 
@@ -34,6 +34,8 @@ open Hints
 
 (** Hint database named "typeclass_instances", now created directly in Auto *)
 
+(** Options handling *)
+
 let typeclasses_debug = ref 0
 let typeclasses_depth = ref None
 
@@ -69,7 +71,7 @@ let set_typeclasses_unif_compat_string d =
   set_typeclasses_unif_compat (get_compat_version d)
 let get_typeclasses_unif_compat_string () =
   Flags.pr_version (get_typeclasses_unif_compat ())
-          
+
 let typeclasses_compat = ref Flags.Current
 let set_typeclasses_compat d = (:=) typeclasses_compat d
 let get_typeclasses_compat () = !typeclasses_compat
@@ -92,7 +94,7 @@ let set_typeclasses_depth d = (:=) typeclasses_depth d
 let get_typeclasses_depth () = !typeclasses_depth
 
 open Goptions
-     
+
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -111,7 +113,7 @@ let _ =
       optkey   = ["Typeclasses";"Limit";"Intros"];
       optread  = get_typeclasses_limit_intros;
       optwrite = set_typeclasses_limit_intros; }
-    
+
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -184,44 +186,13 @@ let set_typeclasses_depth =
       optread  = get_typeclasses_depth;
       optwrite = set_typeclasses_depth; }
 
-let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
-    
-(** We transform the evars that are concerned by this resolution
-    (according to predicate p) into goals.
-    Invariant: function p only manipulates and returns undefined evars *)
-
-let top_sort evm undefs =
-  let l' = ref [] in
-  let tosee = ref undefs in
-  let rec visit ev evi = 
-    let evs = Evarutil.undefined_evars_of_evar_info evm evi in
-      Evar.Set.iter (fun ev -> 
-	if Evar.Map.mem ev !tosee then 
-	  visit ev (Evar.Map.find ev !tosee)) evs;
-      tosee := Evar.Map.remove ev !tosee;
-      l' := ev :: !l';
-  in
-    while not (Evar.Map.is_empty !tosee) do
-      let ev, evi = Evar.Map.min_binding !tosee in
-	visit ev evi
-    done;
-    List.rev !l'
-
-let evars_to_goals p evm =
-  let goals = ref Evar.Map.empty in
-  let map ev evi =
-    let evi, goal = p evm ev evi in
-    let () = if goal then goals := Evar.Map.add ev evi !goals in
-    evi
-  in
-  let evm = Evd.raw_map_undefined map evm in
-  if Evar.Map.is_empty !goals then None
-  else Some (!goals, evm)
+let pr_ev evs ev =
+  Printer.pr_constr_env (Goal.V82.env evs ev) evs
+                        (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
 (** Typeclasses instance search tactic / eauto *)
 
 open Auto
-
 open Unification
 
 let auto_core_unif_flags st freeze = {
@@ -239,7 +210,7 @@ let auto_core_unif_flags st freeze = {
   modulo_eta = !typeclasses_modulo_eta;
 }
 
-let auto_unif_flags freeze st = 
+let auto_unif_flags freeze st =
   let fl = auto_core_unif_flags st freeze in
   { core_unify_flags = fl;
     merge_unify_flags = fl;
@@ -248,25 +219,6 @@ let auto_unif_flags freeze st =
     resolve_evars = false
 }
 
-(* TODO: move, exported tactic in g_class *)
-let rec eq_constr_mod_evars x y =
-  match kind_of_term x, kind_of_term y with
-  | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true
-  | _, _ -> compare_constr eq_constr_mod_evars x y
-
-let progress_evars t =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let concl = Proofview.Goal.concl gl in
-    let check =
-      Proofview.Goal.nf_enter { enter = begin fun gl' ->
-        let newconcl = Proofview.Goal.concl gl' in
-        if eq_constr_mod_evars concl newconcl
-        then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
-        else Proofview.tclUNIT ()
-      end }
-    in t <*> check
-  end }
-
 let e_give_exact flags poly (c,clenv) gl =
   let (c, _, _) = c in
   let c, gl =
@@ -274,7 +226,7 @@ let e_give_exact flags poly (c,clenv) gl =
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
       let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-	c, {gl with sigma = evd}
+        c, {gl with sigma = evd}
     else c, gl
   in
   let t1 = pf_unsafe_type_of gl c in
@@ -292,17 +244,15 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
     Clenvtac.clenv_refine false ~with_classes:false clenv'
   end }
 
-exception ReachedLimitEx
-exception NotApplicableEx  
-                                 
-let unify_resolve_newcl poly flags =
-  let open Clenv in 
+(** Application of a lemma using [refine] instead of the old [w_unify] *)
+let unify_resolve_refine poly flags =
+  let open Clenv in
   { enter = begin fun gls ((c, t, ctx),n,clenv) ->
     let env = Proofview.Goal.env gls in
     let concl = Proofview.Goal.concl gls in
     Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
       let sigma = Sigma.to_evar_map sigma in
-      let sigma, term, ty = 
+      let sigma, term, ty =
         if poly then
           let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
           let map c = Vars.subst_univs_level_constr subst c in
@@ -319,13 +269,15 @@ let unify_resolve_newcl poly flags =
         if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
                                       evdref cl.cl_concl concl) then
           Type_errors.error_actual_type env
-                                        {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
-                                        concl;
+            {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
+            concl;
         !evdref
       in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
   end }
 
-                                 
+(** Dealing with goals of the form A -> B and hints of the form
+  C -> A -> B. In the
+*)
 let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some (None, clenv)
@@ -335,7 +287,7 @@ let clenv_of_prods poly nprods (c, clenv) gl =
     let diff = nb_prod ty - nprods in
       if Pervasives.(>=) diff 0 then
         (* Was Some clenv... *)
-	Some (Some diff,
+        Some (Some diff,
               Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
       else None
 
@@ -349,7 +301,7 @@ let with_prods nprods poly (c, clenv) f =
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
                    else Tacticals.New.tclZEROMSG (str"Not enough premisses") end }
-                                                              
+
 let matches_pattern concl pat =
   let matches env sigma =
     match pat with
@@ -357,8 +309,8 @@ let matches_pattern concl pat =
     | Some pat ->
        let sigma = Sigma.to_evar_map sigma in
        if Constr_matching.is_matching env sigma pat concl then
-	 Proofview.tclUNIT ()
-       else 
+         Proofview.tclUNIT ()
+       else
          Tacticals.New.tclZEROMSG (str "conclPattern")
   in
    Proofview.Goal.enter { enter = fun gl ->
@@ -375,7 +327,7 @@ let matches_pattern concl pat =
     in independent goals or the conclusion are turned into subgoals iff
     they are of typeclass kind.
   - The remaining dependent evars not of typeclass type are shelved,
-    and resolution must fill them for it to succeed, otherwise we 
+    and resolution must fill them for it to succeed, otherwise we
     backtrack.
  *)
 
@@ -390,14 +342,13 @@ let shelve_dependencies gls =
   (if !typeclasses_debug > 1 then
      Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls);
    shelve_goals gls)
-                               
-(** Hack to properly solve dependent evars that are typeclasses *)
 
+(** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db =
   let open Tacticals.New in
   let open Tacmach.New in
   let trivial_fail =
-    Proofview.Goal.nf_enter { enter = 
+    Proofview.Goal.nf_enter { enter =
     begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -408,13 +359,13 @@ let rec e_trivial_fail_db only_classes db_list local_db =
       end }
   in
   let trivial_resolve =
-    Proofview.Goal.nf_enter { enter = 
+    Proofview.Goal.nf_enter { enter =
     begin fun gl ->
     let tacs = e_trivial_resolve db_list local_db only_classes
                                  (project gl) (pf_concl gl) in
       tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
-    end}                   
-  in               
+    end}
+  in
   let tacl =
     Eauto.registered_e_assumption ::
     (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve])
@@ -425,24 +376,24 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
   let open Proofview.Notations in
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
-  let freeze = 
+  let freeze =
     try
       let cl = Typeclasses.class_info (fst hdc) in
-	if cl.cl_strict then
-	  Evd.evars_of_term concl
-	else Evar.Set.empty
+        if cl.cl_strict then
+          Evd.evars_of_term concl
+        else Evar.Set.empty
     with e when Errors.noncritical e -> Evar.Set.empty
   in
   let hintl =
     List.map_append
       (fun db ->
-	let tacs = 
-	  if Hint_db.use_dn db then (* Using dnet *)
-	    Hint_db.map_eauto hdc concl db
-	  else Hint_db.map_existential hdc concl db
-	in
-	let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
-	  List.map (fun x -> (flags, x)) tacs)
+        let tacs =
+          if Hint_db.use_dn db then (* Using dnet *)
+            Hint_db.map_eauto hdc concl db
+          else Hint_db.map_existential hdc concl db
+        in
+        let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
+          List.map (fun x -> (flags, x)) tacs)
       (local_db::db_list)
   in
   let tac_of_hint =
@@ -454,7 +405,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
                with_prods nprods poly (term,cl)
                           ({ enter = fun gl clenv ->
                              (matches_pattern concl p) <*>
-                               ((unify_resolve_newcl poly flags).enter gl clenv)})
+                               ((unify_resolve_refine poly flags).enter gl clenv)})
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -469,14 +420,14 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
              let tac = (with_prods nprods poly (term,cl)
                   ({ enter = fun gl clenv ->
                              (matches_pattern concl p) <*>
-                               ((unify_resolve_newcl poly flags).enter gl clenv)})) in
+                               ((unify_resolve_refine poly flags).enter gl clenv)})) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
                with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
              if get_typeclasses_compat () = Flags.V8_5 then
                Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
-             else 
+             else
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
       | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
@@ -498,9 +449,9 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
            str " with pattern " ++ Printer.pr_constr_pattern pat
         | _ -> mt ()
       in
-	match repr_hint t with
-	| Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
-	| _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
+        match repr_hint t with
+        | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
+        | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db only_classes sigma concl =
@@ -515,37 +466,62 @@ let e_possible_resolve db_list local_db only_classes sigma concl =
       (decompose_app_bound concl) false only_classes sigma concl
   with Bound | Not_found -> []
 
+let cut_of_hints h =
+  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+
 let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
 let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
-type autoinfo = { hints : hint_db; is_evar: existential_key option;
-		  only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit
-type 'ans fk = failure -> '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
+let is_Prop env sigma concl =
+  let ty = Retyping.get_type_of env sigma concl in
+  match kind_of_term ty with
+  | Sort (Prop Null) -> true
+  | _ -> false
 
-type atac = auto_result tac
+let is_unique env concl =
+  try
+    let (cl,u), args = dest_class_app env concl in
+    cl.cl_unique
+  with e when Errors.noncritical e -> false
 
-(* Some utility types to avoid the need of -rectypes *)
+(** Sort the undefined variables from the least-dependent to most dependent. *)
+let top_sort evm undefs =
+  let l' = ref [] in
+  let tosee = ref undefs in
+  let rec visit ev evi =
+    let evs = Evarutil.undefined_evars_of_evar_info evm evi in
+      Evar.Set.iter (fun ev ->
+        if Evar.Map.mem ev !tosee then
+          visit ev (Evar.Map.find ev !tosee)) evs;
+      tosee := Evar.Map.remove ev !tosee;
+      l' := ev :: !l';
+  in
+    while not (Evar.Map.is_empty !tosee) do
+      let ev, evi = Evar.Map.min_binding !tosee in
+        visit ev evi
+    done;
+    List.rev !l'
 
-type 'a optionk =
-  | Nonek
-  | Somek of 'a * 'a optionk fk
+(** We transform the evars that are concerned by this resolution
+    (according to predicate p) into goals.
+    Invariant: function p only manipulates and returns undefined evars
+*)
 
-type ('a,'b) optionk2 =
-  | Nonek2 of failure
-  | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+let evars_to_goals p evm =
+  let goals = ref Evar.Map.empty in
+  let map ev evi =
+    let evi, goal = p evm ev evi in
+    let () = if goal then goals := Evar.Map.add ev evi !goals in
+    evi
+  in
+  let evm = Evd.raw_map_undefined map evm in
+  if Evar.Map.is_empty !goals then None
+  else Some (!goals, evm)
 
+(** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
   let open Context.Named.Declaration in
   let id = get_id decl in
@@ -556,10 +532,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       | Const (c,_) -> is_class (ConstRef c)
       | Ind (i,_) -> is_class (IndRef i)
       | _ ->
-	  let env' = Environ.push_rel_context ctx env in
-	  let ty' = whd_betadeltaiota env' ar in
-	       if not (Term.eq_constr ty' ar) then iscl env' ty'
-	       else false
+          let env' = Environ.push_rel_context ctx env in
+          let ty' = whd_betadeltaiota env' ar in
+               if not (Term.eq_constr ty' ar) then iscl env' ty'
+               else false
   in
   let is_class = iscl env cty in
   let keep = not only_classes || is_class in
@@ -567,674 +543,728 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       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 (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
-		  (true,false,Flags.is_verbose()) pri false
-		 (IsConstr (c,Univ.ContextSet.empty)))
-	       hints)
-	else []
+        if is_class then
+          let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+            (List.map_append
+               (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
+                  (true,false,Flags.is_verbose()) pri false
+                 (IsConstr (c,Univ.ContextSet.empty)))
+               hints)
+        else []
       in
         (hints @ List.map_filter
-	 (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) 
-	   with Failure _ | UserError _ -> None)
-	 [make_exact_entry ~name env sigma pri false; 
-	  make_apply_entry ~name env sigma flags pri false])
+         (fun f -> try Some (f (c, cty, Univ.ContextSet.empty))
+           with Failure _ | UserError _ -> None)
+         [make_exact_entry ~name env sigma pri false;
+          make_apply_entry ~name env sigma flags pri false])
     else []
 
-let pf_filtered_hyps gls =
-  Goal.V82.hyps gls.Evd.sigma (sig_it gls)
-
 let make_hints g st only_classes sign =
-  let paths, hintlist =
+  let hintlist =
     List.fold_left
-    (fun (paths, hints) hyp ->
-      let consider =
-        let open Context.Named.Declaration in
-	try let t = Global.lookup_named (get_id hyp) |> get_type in
-	      (* Section variable, reindex only if the type changed *)
-	      not (Term.eq_constr t (get_type hyp))
-	with Not_found -> true
-     in
-      if consider then 
-	let path, hint =
-	  PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
-	in
-	  (PathOr (paths, path), hint @ hints)
-      else (paths, hints))
-    (PathEmpty, []) sign
+      (fun hints hyp ->
+        let consider =
+          let open Context.Named.Declaration in
+          try let t = Global.lookup_named (get_id hyp) |> get_type in
+              (* Section variable, reindex only if the type changed *)
+              not (Term.eq_constr t (get_type hyp))
+          with Not_found -> true
+        in
+        if consider then
+          let hint =
+            pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+          in hint @ hints
+        else hints)
+      ([]) sign
   in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
 
-let make_autogoal_hints =
-  let cache = ref (true, Environ.empty_named_context_val, 
-		   Hint_db.empty full_transparent_state true) 
-  in
-    fun only_classes ?(st=full_transparent_state) g ->
-      let sign = pf_filtered_hyps g in
-      let (onlyc, sign', cached_hints) = !cache in
-	if onlyc == only_classes && 
-	  (sign == sign' || Environ.eq_named_context_val sign sign') 
-	  && Hint_db.transparent_state cached_hints == st
-	then
-	  cached_hints
-	else
-	  let hints = make_hints g st only_classes (Environ.named_context_of_val sign)
-          in
-	    cache := (only_classes, 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 -> sk (f gls hints) fk
-      | None -> fk NotApplicable }
-
-let intro_tac : atac =
-  lift_tactic (Proofview.V82.of_tactic Tactics.intro)
-    (fun {it = gls; sigma = s} info ->
-      let gls' =
-	List.map (fun g' ->
-	  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 context) in
-	  let ldb = Hint_db.add_list env s 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 =
-  { 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 }
-
-let merge_failures x y =
-  match x, y with
-  | _, ReachedLimit
-  | ReachedLimit, _ -> ReachedLimit
-  | NotApplicable, NotApplicable -> NotApplicable
-
-let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft sk
-    (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls }
-
-let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft sk
-    (fun f -> (y f).skft sk fk gls) gls }
+(** <= 8.5 resolution *)
+module V85 = struct
 
-let is_Prop env sigma concl =
-  let ty = Retyping.get_type_of env sigma concl in
-  match kind_of_term ty with
-  | Sort (Prop Null) -> true
-  | _ -> false
+  type autoinfo = { hints : hint_db; is_evar: existential_key option;
+                    only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit
+  type 'ans fk = failure -> 'ans
+  type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
+  type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
 
-let is_unique env concl = 
-  try 
-    let (cl,u), args = dest_class_app env concl in
-      cl.cl_unique
-  with e when Errors.noncritical e -> false
+  type auto_result = autogoal list sigma
 
-let needs_backtrack env evd oev concl =
-  if Option.is_empty oev || is_Prop env evd concl then
-    occur_existential concl
-  else true
+  type atac = auto_result tac
 
-type newautoinfo =
-  { search_depth : int list;
-    last_tac : Pp.std_ppcmds Lazy.t;
-    search_dep : bool;
-    search_cut : hints_path;
-    search_hints : hint_db; }
+  (* Some utility types to avoid the need of -rectypes *)
 
-let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty,
-		          Hint_db.empty full_transparent_state true)
+  type 'a optionk =
+    | Nonek
+    | Somek of 'a * 'a optionk fk
 
-let make_autogoal_hints' only_classes ?(st=full_transparent_state) g =
-  let open Proofview in
-  let open Tacmach.New in
-  let sign = Goal.hyps g in
-  let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
-  let cwd = Lib.cwd () in
-  if DirPath.equal cwd dir &&
-     (onlyc == only_classes) && 
-       Context.Named.equal sign sign' &&
-         Hint_db.transparent_state cached_hints == st
-  then cached_hints
-  else
-    let hints = make_hints {it = Goal.goal g; sigma = project g}
-                           st only_classes sign
+  type ('a,'b) optionk2 =
+    | Nonek2 of failure
+    | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+
+  let pf_filtered_hyps gls =
+    Goal.V82.hyps gls.Evd.sigma (sig_it gls)
+
+  let make_autogoal_hints =
+    let cache = ref (true, Environ.empty_named_context_val,
+                     Hint_db.empty full_transparent_state true)
     in
-    autogoal_cache := (cwd, only_classes, sign, hints); hints
-    
-let make_autogoal' ?(st=full_transparent_state) only_classes dep cut i g =
-  let hints = make_autogoal_hints' only_classes ~st g in
-  let info = { search_hints = hints;
-               search_depth = [i]; last_tac = lazy (str"none");
-               search_dep = dep;
-               search_cut = cut } in
-  info
-                 
-let needs_backtrack' env evd unique concl =
-  if unique || is_Prop env evd concl then
-    occur_existential concl
-  else true
-
-let merge_exceptions e e' =
-  match fst e, fst e' with
-  | ReachedLimitEx, _ -> e
-  | _, ReachedLimitEx -> e'
-  | _, _ -> e
-
-let new_hints_tac_gl only_classes hints info kont gl
-    : unit Proofview.tactic
-  =
-  let open Proofview in
-  let open Proofview.Notations in
-  let env = Goal.env gl in
-  let concl = Goal.concl gl in
-  let sigma = Goal.sigma gl in
-  let s = Sigma.to_evar_map sigma in
-  let unique = not info.search_dep || is_unique env concl in
-  let backtrack = needs_backtrack' env s unique concl in
-  if !typeclasses_debug > 0 then
-    Feedback.msg_debug
-      (pr_depth info.search_depth ++ str": looking for " ++
-	 Printer.pr_constr_env (Goal.env gl) s concl ++
-         (if backtrack then str" with backtracking"
-          else str" without backtracking"));
-  let poss = e_possible_resolve hints info.search_hints only_classes s concl in
-  (* If no goal depends on the solution of this one or the
-     instances are irrelevant/assumed to be unique, then 
-     we don't need to backtrack, as long as no evar appears in the goal 
-     This is an overapproximation. Evars could appear in this goal only
-     and not any other *)
-  let ortac = if backtrack then Proofview.tclOR else Proofview.tclORELSE in
-  let idx = ref 1 in
-  let foundone = ref false in
-  let rec aux e = function
-    | (tac, pat, b, name, pp) :: tl ->
-       let derivs = path_derivate info.search_cut name in
-       (if !typeclasses_debug > 1 then
-	  Feedback.msg_debug
-            (pr_depth (!idx :: info.search_depth) ++ str": trying " ++
-               Lazy.force pp ++
-               (if !foundone != true then
-                  str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
-                else mt ())));
-       let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
-         let sigma' = Goal.sigma gl' in
-         let s' = Sigma.to_evar_map sigma' in
-         let _concl = Goal.concl gl' in
-         if !typeclasses_debug > 0 then
-	   Feedback.msg_debug
-             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
-                pr_ev s' (Proofview.Goal.goal gl'));
-         let hints' =
-           if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl))
-	   then
-             let st = Hint_db.transparent_state info.search_hints in
-             make_autogoal_hints' only_classes ~st gl'
-	   else info.search_hints
-         in
-         let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in
-         let info' = 
-	   { search_depth = succ j :: i :: info.search_depth;
-             last_tac = pp;
-             search_dep = dep';
-	     search_hints = hints';
-	     search_cut = derivs }
-         in
-         kont info' }
-       in
-       let rec result (shelf, ()) i k =
-         foundone := true;
-         Proofview.Unsafe.tclGETGOALS >>= fun gls ->
-         let j = List.length gls in
-         (if !typeclasses_debug > 0 then
-	    Feedback.msg_debug
-              (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
-	       ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
-               ++ str", " ++ int j ++ str" subgoal(s)" ++
-                 (Option.cata (fun k -> str " in addition to the first " ++ int k)
-                              (mt()) k)));
+    fun only_classes ?(st=full_transparent_state) g ->
+    let sign = pf_filtered_hyps g in
+    let (onlyc, sign', cached_hints) = !cache in
+    if onlyc == only_classes &&
+         (sign == sign' || Environ.eq_named_context_val sign sign')
+         && Hint_db.transparent_state cached_hints == st
+    then
+      cached_hints
+    else
+      let hints = make_hints g st only_classes (Environ.named_context_of_val sign)
+      in
+      cache := (only_classes, 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 -> sk (f gls hints) fk
+             | None -> fk NotApplicable }
+
+  let intro_tac : atac =
+    let tac {it = gls; sigma = s} info =
+      let gls' =
+        List.map (fun g' ->
+            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 context) in
+            let ldb = Hint_db.add_list env s hint info.hints in
+            (g', { info with is_evar = None; hints = ldb;
+                             auto_last_tac = lazy (str"intro") })) gls
+      in {it = gls'; sigma = s;}
+    in
+    lift_tactic (Proofview.V82.of_tactic Tactics.intro) tac
+
+  let normevars_tac : atac =
+    { 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 }
+
+  let merge_failures x y =
+    match x, y with
+    | _, ReachedLimit
+      | ReachedLimit, _ -> ReachedLimit
+    | NotApplicable, NotApplicable -> NotApplicable
+
+  let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
+    { skft = fun sk fk gls -> x.skft sk
+      (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls }
+
+  let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac =
+    { skft = fun sk fk gls -> x.skft sk
+      (fun f -> (y f).skft sk fk gls) gls }
+
+  let needs_backtrack env evd oev concl =
+    if Option.is_empty oev || is_Prop env evd concl then
+      occur_existential concl
+    else true
+
+  let hints_tac hints sk fk {it = gl,info; sigma = s} =
+    let env = Goal.V82.env s gl in
+    let concl = Goal.V82.concl s gl in
+    let tacgl = {it = gl; sigma = s;} in
+    let poss = e_possible_resolve hints info.hints info.only_classes s concl in
+    let unique = is_unique env concl in
+    let rec aux i foundone = function
+      | (tac, _, b, name, pp) :: tl ->
+         let derivs = path_derivate info.auto_cut name in
          let res =
-           if j = 0 then tclUNIT ()
-           else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
+           try
+             if path_matches derivs [] then None
+             else Some (Proofview.V82.of_tactic tac tacgl)
+           with e when catchable e -> None
          in
-         let finish = 
-           tclEVARMAP >>= fun sigma ->
-           let filter ev =
-             try
-               let evi = Evd.find_undefined sigma ev in
-               if only_classes then
-                 Some (ev, is_class_type sigma (Evd.evar_concl evi))
-               else Some (ev, true)
-             with Not_found -> None
-           in
-           let remaining = CList.map_filter filter shelf in
-           if !typeclasses_debug > 1 then
-             Feedback.msg_debug
-               (pr_depth (i :: info.search_depth) ++
-                  str": after " ++ Lazy.force pp ++ str" finished, " ++
-                  int (List.length remaining) ++
-                  str " goals are shelved and unsolved ( " ++
-                  prlist_with_sep spc
-                    (fun ev -> int (Evar.repr ev) ++ spc () ++
-                              pr_ev sigma ev) (List.map fst remaining) ++ str")");
-           begin
-             (* Some existentials produced by the original tactic were not solved
-                in the subgoals, turn them into subgoals now. *)
-             let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
-             let shelved = List.map fst shelved and goals = List.map fst goals in
-             if !typeclasses_debug > 1 then
-               Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++
-                            prlist_with_sep spc (pr_ev sigma) goals);
-             shelve_goals shelved <*>
-               (if List.is_empty goals then tclUNIT ()
-                else with_shelf (Unsafe.tclNEWGOALS goals) >>=
-                       fun s -> result s i (Some (Option.default 0 k + j)))
-           end
-         in res <*> finish
+         (match res with
+          | None -> aux i foundone tl
+          | Some {it = gls; sigma = s';} ->
+             if !typeclasses_debug > 0 then
+               Feedback.msg_debug
+                 (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+                  ++ str" on" ++ spc () ++ pr_ev s gl);
+             let sgls =
+               evars_to_goals
+                 (fun evm ev evi ->
+                   if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) &&
+                        (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') ->
+                  if not !typeclasses_dependency_order then
+                    (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s')
+                  else
+                    (* Reorder with dependent subgoals. *)
+                    let evm = List.fold_left
+                                (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in
+                    let gls = top_sort s' evm in
+                    (List.map (fun ev -> Some ev, ev) gls, 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
+             let fk' =
+               (fun e ->
+                 let do_backtrack =
+                   if unique then occur_existential concl
+                   else if info.unique then true
+                   else if List.is_empty gls' then
+                     needs_backtrack env s' info.is_evar concl
+                   else true
+                 in
+                 let e' = match foundone with None -> e
+                                            | Some e' -> merge_failures e e' in
+                 if !typeclasses_debug > 0 then
+                   Feedback.msg_debug
+                     ((if do_backtrack then str"Backtracking after "
+                       else str "Not backtracking after ")
+                      ++ Lazy.force pp);
+                 if do_backtrack then aux (succ i) (Some e') tl
+                 else fk e')
+             in
+             sk glsv fk')
+      | [] ->
+         if foundone == None && !typeclasses_debug > 0 then
+           Feedback.msg_debug
+             (pr_depth info.auto_depth ++ str": no match for " ++
+                Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
+                spc () ++ str ", " ++ int (List.length poss) ++
+                str" possibilities");
+         match foundone with
+         | Some e -> fk e
+         | None -> fk NotApplicable
+    in aux 1 None poss
+
+  let hints_tac hints =
+  { skft = fun sk fk gls -> hints_tac hints sk fk gls }
+
+  let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
+    let rec aux s (acc : autogoal list list) fk = function
+      | (gl,info) :: gls ->
+         Control.check_for_interrupt ();
+         (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 fk'' =
+                   if not info.unique && List.is_empty gls' &&
+                        not (needs_backtrack (Goal.V82.env s gl) s
+                                           info.is_evar (Goal.V82.concl s gl))
+                   then fk
+                   else fk'
+                 in
+                 aux s' (gls'::acc) fk'' gls)
+               fk {it = (gl,info); sigma = s; })
+      | [] -> Somek2 (List.rev acc, s, fk)
+    in fun {it = gls; sigma = s; } fk ->
+       let rec aux' = function
+         | Nonek2 e -> fk e
+         | Somek2 (res, s', fk') ->
+            let goals' = List.concat res in
+            sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e))
+       in aux' (aux s [] (fun e -> Nonek2 e) gls)
+
+  let then_tac (first : atac) (second : atac) : atac =
+    { skft = fun sk fk -> first.skft (then_list second sk) fk }
+
+  let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
+    t.skft (fun x _ -> Some x) (fun _ -> None) gl
+
+  type run_list_res = auto_result optionk
+
+  let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
+    (then_list t (fun x fk -> Somek (x, fk)))
+      gl
+      (fun _ -> Nonek)
+
+  let fail_tac reason : atac =
+    { skft = fun sk fk _ -> fk reason }
+
+  let rec fix (t : 'a tac) : 'a tac =
+    then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
+
+  let rec fix_limit limit (t : 'a tac) : 'a tac =
+    if Int.equal limit 0 then fail_tac ReachedLimit
+    else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
+
+  let fix_iterative t =
+    let rec aux depth =
+      or_else_tac (fix_limit depth t)
+                  (function
+                   | NotApplicable as e -> fail_tac e
+                   | ReachedLimit -> aux (succ depth))
+    in aux 1
+
+  let fix_iterative_limit limit (t : 'a tac) : 'a tac =
+    let rec aux depth =
+      if Int.equal limit depth then fail_tac ReachedLimit
+      else or_tac (fix_limit depth t)
+                  { skft = fun sk fk -> (aux (succ depth)).skft sk fk }
+    in aux 1
+
+  let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state)
+                    cut ev g =
+    let hints = make_autogoal_hints only_classes ~st g in
+    (g.it, { hints = hints ; is_evar = ev; unique = unique;
+             only_classes = only_classes; auto_depth = [];
+             auto_last_tac = lazy (str"none");
+             auto_path = []; auto_cut = cut })
+
+
+  let make_autogoals ?(only_classes=true) ?(unique=false)
+                     ?(st=full_transparent_state) hints gs evm' =
+    let cut = cut_of_hints hints in
+    let gl i g =
+      let (gl, auto) = make_autogoal ~only_classes ~unique
+                                     ~st cut (Some g) {it = g; sigma = evm'; } in
+      (gl, { auto with auto_depth = [i]})
+    in { it = List.map_i gl 1 gs; sigma = evm' }
+
+  let get_result r =
+    match r with
+    | Nonek -> None
+    | Somek (gls, fk) -> Some (gls.sigma,fk)
+
+  let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals =
+         if !typeclasses_dependency_order then
+           top_sort evm' goals
+         else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
        in
-       if path_matches derivs [] then aux e tl
-       else ortac (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None)
-                  (fun e' -> aux (merge_exceptions e e') tl)
-    | [] ->
-       if !foundone == false && !typeclasses_debug > 0 then
-         Feedback.msg_debug
-           (pr_depth info.search_depth ++ str": no match for " ++
-              Printer.pr_constr_env (Goal.env gl) s concl ++
-	      spc () ++ str ", " ++ int (List.length poss) ++
-              str" possibilities");
-       match e with
-       | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
-       | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx
-  in
-  if backtrack then aux (NotApplicableEx,Exninfo.null) poss
-  else tclONCE (aux (NotApplicableEx,Exninfo.null) poss)
-                    
-let new_hints_tac cl hints info kont : unit Proofview.tactic =
-  Proofview.Goal.nf_enter
-    { enter = fun gl -> new_hints_tac_gl cl hints info kont gl }
-
-let cut_of_hints h =
-  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+       let res = run_list_tac tac p goals
+           (make_autogoals ~only_classes ~unique ~st hints goals evm') in
+       match get_result res with
+       | None -> raise Not_found
+       | Some (evm', fk) ->
+          Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk)
 
-let intro_tac'' only_classes info kont gl =
-  let open Proofview in
-  let open Proofview.Notations in
-  let env = Goal.env gl in
-  let sigma = Goal.sigma gl in
-  let s = Sigma.to_evar_map sigma in
-  let decl = Tacmach.New.pf_last_hyp gl in
-  let hint =
-    make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
-	             (true,false,false) only_classes None decl in
-  let ldb = Hint_db.add_list env s hint info.search_hints in
-  let info' =
-    { info with search_hints = ldb; last_tac = lazy (str"intro") }
-  in kont info'
-             
-let intro_tac' only_classes info kont =
-  Proofview.tclBIND Tactics.intro
-   (fun _ ->
-     Proofview.Goal.nf_enter { enter = fun gl -> intro_tac'' only_classes info kont gl })
-
-let rec eauto_tac' only_classes hints limit depth =
-  let kont info =
-    Proofview.numgoals >>= fun i ->
-    if !typeclasses_debug > 1 then
-      Feedback.msg_debug
-        (str"calling eauto recursively at depth " ++ int (succ depth)
-         ++ str" on " ++ int i ++ str" subgoals");
-    eauto_tac' only_classes hints limit (succ depth) info
-  in
-  fun info ->
-  if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx
-  else Proofview.tclOR (new_hints_tac only_classes hints info kont)
-    (fun e -> Proofview.tclOR (intro_tac' only_classes info kont)
-    (fun e' -> let (e, info) = merge_exceptions e e' in
-            Proofview.tclZERO ~info e))
-                                                    
-   
-let new_eauto_tac_gl ?st only_classes dep hints limit i sigma gls gl :
-      unit Proofview.tactic =
-  let open Proofview in
-  let open Proofview.Notations in
-  let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
-  let info = make_autogoal' ?st only_classes dep (cut_of_hints hints) i gl in
-  eauto_tac' only_classes hints limit 1 info
+  let eauto_tac hints =
+    then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
 
-exception HasShelvedGoals
-             
-let new_eauto_tac ?(st=full_transparent_state) only_classes dep hints limit : unit Proofview.tactic =
-  let open Proofview in
-  let eautotac sigma gls i =
-    Goal.nf_enter
-      { enter = fun gl ->
-                new_eauto_tac_gl ~st only_classes dep hints limit (succ i) sigma gls gl }
-  in
-  Proofview.Unsafe.tclGETGOALS >>= fun gls ->
-     Proofview.tclEVARMAP >>= fun sigma ->
-     let j = List.length gls in
-     (tclDISPATCH
-        (List.init j (fun i -> eautotac sigma gls i)))
-       
-let fix_iterative t =
-  let rec aux depth =
-    Proofview.tclOR (t depth)
-      (function 
-       | (ReachedLimitEx,_) -> aux (succ depth)
-       | (e,ie) -> Proofview.tclZERO ~info:ie e)
-  in aux 1
-
-let fix_iterative_limit limit t =
-  let open Proofview in
-  let rec aux depth =
-    if Int.equal depth (succ limit) then tclZERO ReachedLimitEx
-    else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth)
-                                 | (e,ie) -> Proofview.tclZERO ~info:ie e)
-               
-  in aux 1
-
-let new_eauto_tac ?(st=full_transparent_state) only_classes ?limit dep hints =
-  let tac =
+  let eauto_tac depth hints =
     if get_typeclasses_iterative_deepening () then
-      match limit with
-      | None ->
-         fix_iterative (new_eauto_tac ~st only_classes dep hints)
-      | Some l ->
-         fix_iterative_limit l (new_eauto_tac ~st only_classes dep hints)
+      match depth with
+      | None -> fix_iterative (eauto_tac hints)
+      | Some depth -> fix_iterative_limit depth (eauto_tac hints)
     else
-      let limit = match limit with None -> -1 | Some d -> d in
-      new_eauto_tac ~st only_classes dep hints limit
-  in
-  let error (e, ie) =
-    match e with
-    | ReachedLimitEx ->
-       Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
-    | NotApplicableEx ->
-       Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
-                                  (if Option.is_empty limit then mt()
-                                   else str" without reaching its limit"))
-    | e -> Proofview.tclZERO ~info:ie e
-  in Proofview.tclORELSE tac error
-
-let run_on_evars ?(unique=false) p evm tac =
-  match evars_to_goals p evm with
-  | None -> None (* This happens only because there's no evar having p *)
-  | Some (goals, evm') ->
-    let goals = 
-      if !typeclasses_dependency_order then
-	top_sort evm' goals
-      else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+      match depth with
+      | None -> fix (eauto_tac hints)
+      | Some depth -> fix_limit depth (eauto_tac hints)
+
+  let real_eauto ?depth unique st hints p evd =
+    let res =
+      run_on_evars ~st ~unique p evd hints (eauto_tac depth hints)
     in
-    let fgoals = Evd.future_goals evm in
-    let pgoal = Evd.principal_future_goal evm in
-    let _, pv = Proofview.init evm' [] in
-    let pv = Proofview.unshelve goals pv in
-    try
-      let (), pv', (unsafe, shelved, gaveup), _ =
-        Proofview.apply (Global.env ()) tac pv
-      in
-      if Proofview.finished pv' then
-        let evm' = Proofview.return pv' in
-        assert(Evd.fold_undefined (fun ev _ acc ->
-                   let okev = Evd.mem evm ev || List.mem ev shelved in
-                   if not okev then
-                     Feedback.msg_debug
-                       (str "leaking evar " ++ int (Evar.repr ev) ++
-                          spc () ++ pr_ev evm' ev);
-                   acc && okev) evm' true);
-        let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in
-        let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
-        Some evm'
-      else raise Not_found
-    with Logic_monad.TacticFailure _ -> raise Not_found
-
-let real_new_eauto ?limit unique st hints p evd =
-  let eauto_tac = new_eauto_tac ~st true ?limit false hints in
-  let res = run_on_evars ~unique p evd eauto_tac in
     match res with
     | None -> evd
-    | Some evd' -> evd'
-    (* TODO treat unique classes, with exactlyonce *)
-    
-let resolve_all_evars_once' debug limit unique p evd =
-  let db = searchtable_map typeclasses_db in
-    real_new_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd
-
-let hints_tac hints =
-  { skft = fun sk fk {it = gl,info; sigma = s;} ->
-      let env = Goal.V82.env s gl in
-      let concl = Goal.V82.concl s gl in
-      let tacgl = {it = gl; sigma = s;} in
-      let poss = e_possible_resolve hints info.hints info.only_classes s concl in
-      let unique = is_unique env concl in
-      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 (Proofview.V82.of_tactic tac tacgl)
-	  with e when catchable e -> None
-	in
-	  (match res with
-	  | None -> aux i foundone tl
-	  | Some {it = gls; sigma = s';} ->
-	    if !typeclasses_debug > 0 then
-	      Feedback.msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
-			 ++ str" on" ++ spc () ++ pr_ev s gl);
-	    let sgls =
-	      evars_to_goals
-		(fun evm ev evi ->
-		  if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) &&
-		    (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') ->
-		  if not !typeclasses_dependency_order then
-		    (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s')
-		  else 
- 		    (* Reorder with dependent subgoals. *)
-		    let evm = List.fold_left 
-		      (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in
-		    let gls = top_sort s' evm in
-		      (List.map (fun ev -> Some ev, ev) gls, 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
-	    let fk' =
-	      (fun e ->
-		let do_backtrack =
-		  if unique then occur_existential concl
-		  else if info.unique then true
-		  else if List.is_empty gls' then 
-		    needs_backtrack env s' info.is_evar concl
-		  else true
-		in
-		let e' = match foundone with None -> e | Some e' -> merge_failures e e' in
-		  if !typeclasses_debug > 0 then
-		    Feedback.msg_debug 
-		      ((if do_backtrack then str"Backtracking after "
-			else str "Not backtracking after ")
-		       ++ Lazy.force pp);
-		  if do_backtrack then aux (succ i) (Some e') tl
-		  else fk e')
-	    in
-	      sk glsv fk')
+    | Some (evd', fk) ->
+       if unique then
+         (match get_result (fk NotApplicable) with
+          | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions"
+          | None -> evd')
+       else evd'
+
+  let resolve_all_evars_once debug depth unique p evd =
+    let db = searchtable_map typeclasses_db in
+    real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
+
+  let eauto85 ?(only_classes=true) ?st depth 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 depth hints) gl with
+    | None -> raise Not_found
+    | Some {it = goals; sigma = s; } ->
+       {it = List.map fst goals; sigma = s;}
+
+end
+
+(** 8.6 resolution *)
+module Search = struct
+  type autoinfo =
+    { search_depth : int list;
+      last_tac : Pp.std_ppcmds Lazy.t;
+      search_dep : bool;
+      search_only_classes : bool;
+      search_cut : hints_path;
+      search_hints : hint_db; }
+
+  let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty,
+                            Hint_db.empty full_transparent_state true)
+
+  let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
+    let open Proofview in
+    let open Tacmach.New in
+    let sign = Goal.hyps g in
+    let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
+    let cwd = Lib.cwd () in
+    if DirPath.equal cwd dir &&
+         (onlyc == only_classes) &&
+           Context.Named.equal sign sign' &&
+             Hint_db.transparent_state cached_hints == st
+    then cached_hints
+    else
+      let hints = make_hints {it = Goal.goal g; sigma = project g}
+                             st only_classes sign
+      in
+      autogoal_cache := (cwd, only_classes, sign, hints); hints
+
+  let make_autogoal ?(st=full_transparent_state) only_classes dep cut i g =
+    let hints = make_autogoal_hints only_classes ~st g in
+    { search_hints = hints;
+      search_depth = [i]; last_tac = lazy (str"none");
+      search_dep = dep;
+      search_only_classes = only_classes;
+      search_cut = cut }
+
+  let needs_backtrack env evd unique concl =
+    if unique || is_Prop env evd concl then
+      occur_existential concl
+    else true
+
+  (** In the proof engine failures are represented as exceptions *)
+  exception ReachedLimitEx
+  exception NotApplicableEx
+
+  let merge_exceptions e e' =
+    match fst e, fst e' with
+    | ReachedLimitEx, _ -> e
+    | _, ReachedLimitEx -> e'
+    | _, _ -> e
+
+  let hints_tac_gl hints info kont gl : unit Proofview.tactic =
+    let open Proofview in
+    let open Proofview.Notations in
+    let env = Goal.env gl in
+    let concl = Goal.concl gl in
+    let sigma = Goal.sigma gl in
+    let s = Sigma.to_evar_map sigma in
+    let unique = not info.search_dep || is_unique env concl in
+    let backtrack = needs_backtrack env s unique concl in
+    if !typeclasses_debug > 0 then
+      Feedback.msg_debug (pr_depth info.search_depth ++ str": looking for " ++
+                   Printer.pr_constr_env (Goal.env gl) s concl ++
+                   (if backtrack then str" with backtracking"
+                    else str" without backtracking"));
+    let poss =
+      e_possible_resolve hints info.search_hints info.search_only_classes s concl in
+    (* If no goal depends on the solution of this one or the
+       instances are irrelevant/assumed to be unique, then
+       we don't need to backtrack, as long as no evar appears in the goal
+       This is an overapproximation. Evars could appear in this goal only
+       and not any other *)
+    let ortac = if backtrack then Proofview.tclOR else Proofview.tclORELSE in
+    let idx = ref 1 in
+    let foundone = ref false in
+    let rec aux e = function
+      | (tac, pat, b, name, pp) :: tl ->
+         let derivs = path_derivate info.search_cut name in
+         (if !typeclasses_debug > 1 then
+            Feedback.msg_debug (pr_depth (!idx :: info.search_depth) ++ str": trying " ++
+                         Lazy.force pp ++
+                         (if !foundone != true then
+                            str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+                          else mt ())));
+         let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
+            begin
+              let sigma' = Goal.sigma gl' in
+              let s' = Sigma.to_evar_map sigma' in
+              let _concl = Goal.concl gl' in
+              if !typeclasses_debug > 0 then
+                Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
+                             pr_ev s' (Proofview.Goal.goal gl'));
+              let hints' =
+                if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl))
+                then
+                  let st = Hint_db.transparent_state info.search_hints in
+                  make_autogoal_hints info.search_only_classes ~st gl'
+                else info.search_hints
+              in
+              let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in
+              let info' =
+                { search_depth = succ j :: i :: info.search_depth;
+                  last_tac = pp;
+                  search_dep = dep';
+                  search_only_classes = info.search_only_classes;
+                  search_hints = hints';
+                  search_cut = derivs }
+              in
+              kont info' end }
+         in
+         let rec result (shelf, ()) i k =
+           foundone := true;
+           Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+           let j = List.length gls in
+           (if !typeclasses_debug > 0 then
+              Feedback.msg_debug
+                (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
+                 ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+                 ++ str", " ++ int j ++ str" subgoal(s)" ++
+                   (Option.cata (fun k -> str " in addition to the first " ++ int k)
+                                (mt()) k)));
+           let res =
+             if j = 0 then tclUNIT ()
+             else tclDISPATCH
+                    (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
+           in
+           let finish =
+             tclEVARMAP >>= fun sigma ->
+             let filter ev =
+               try
+                 let evi = Evd.find_undefined sigma ev in
+                 if info.search_only_classes then
+                   Some (ev, is_class_type sigma (Evd.evar_concl evi))
+                 else Some (ev, true)
+               with Not_found -> None
+             in
+             let remaining = CList.map_filter filter shelf in
+             if !typeclasses_debug > 1 then
+               Feedback.msg_debug (pr_depth (i :: info.search_depth) ++
+                            str": after " ++ Lazy.force pp ++ str" finished, " ++
+                            int (List.length remaining) ++
+                            str " goals are shelved and unsolved ( " ++
+                            prlist_with_sep spc
+                                            (fun ev -> int (Evar.repr ev) ++ spc () ++
+                                                      pr_ev sigma ev)
+                                            (List.map fst remaining) ++ str")");
+             begin
+               (* Some existentials produced by the original tactic were not solved
+                in the subgoals, turn them into subgoals now. *)
+               let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
+               let shelved = List.map fst shelved and goals = List.map fst goals in
+               if !typeclasses_debug > 1 then
+                 Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++
+                              prlist_with_sep spc (pr_ev sigma) goals);
+               shelve_goals shelved <*>
+                 (if List.is_empty goals then tclUNIT ()
+                  else with_shelf (Unsafe.tclNEWGOALS goals) >>=
+                         fun s -> result s i (Some (Option.default 0 k + j)))
+             end
+           in res <*> finish
+         in
+         if path_matches derivs [] then aux e tl
+         else ortac (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None)
+                    (fun e' -> aux (merge_exceptions e e') tl)
       | [] ->
-	if foundone == None && !typeclasses_debug > 0 then
-	  Feedback.msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
-		       Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
-		       spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities");
-	match foundone with
-	| Some e -> fk e
-	| None -> fk NotApplicable
-      in aux 1 None poss }
-
-let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
-  let rec aux s (acc : autogoal list list) fk = function
-    | (gl,info) :: gls ->
-        Control.check_for_interrupt ();
-	(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 fk'' =
-		   if not info.unique && List.is_empty gls' &&
-		     not (needs_backtrack (Goal.V82.env s gl) s
-			    info.is_evar (Goal.V82.concl s gl))
-		   then fk
-		   else fk'
-		 in
-		   aux s' (gls'::acc) fk'' gls)
-	       fk {it = (gl,info); sigma = s; })
-    | [] -> Somek2 (List.rev acc, s, fk)
-  in fun {it = gls; sigma = s; } fk ->
-    let rec aux' = function
-      | Nonek2 e -> fk e
-      | Somek2 (res, s', fk') ->
-	  let goals' = List.concat res in
-	    sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e))
-    in aux' (aux s [] (fun e -> Nonek2 e) gls)
-
-let then_tac (first : atac) (second : atac) : atac =
-  { skft = fun sk fk -> first.skft (then_list second sk) fk }
-
-let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
-  t.skft (fun x _ -> Some x) (fun _ -> None) gl
-
-type run_list_res = auto_result optionk
-
-let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
-  (then_list t (fun x fk -> Somek (x, fk)))
-    gl
-    (fun _ -> Nonek)
-
-let fail_tac reason : atac =
-  { skft = fun sk fk _ -> fk reason }
-
-let rec fix (t : 'a tac) : 'a tac =
-  then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
-
-let rec fix_limit limit (t : 'a tac) : 'a tac =
-  if Int.equal limit 0 then fail_tac ReachedLimit
-  else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
-
-let fix_iterative t =
-  let rec aux depth =
-    or_else_tac (fix_limit depth t)
-      (function 
-	| NotApplicable as e -> fail_tac e
-	| ReachedLimit -> aux (succ depth))
-  in aux 1
-
-let fix_iterative_limit limit (t : 'a tac) : 'a tac =
-  let rec aux depth =
-    if Int.equal depth limit then fail_tac ReachedLimit
-    else or_tac (fix_limit depth t) { skft = fun sk fk -> (aux (succ depth)).skft sk fk }
-  in aux 1
-
-let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state)
-                  cut ev g =
-  let hints = make_autogoal_hints only_classes ~st g in
-    (g.it, { hints = hints ; is_evar = ev; unique = unique;
-	     only_classes = only_classes; auto_depth = [];
-             auto_last_tac = lazy (str"none");
-	     auto_path = []; auto_cut = cut })
-
-
-let make_autogoals ?(only_classes=true) ?(unique=false) 
-    ?(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 ~unique 
-      ~st cut (Some g) {it = g; sigma = evm'; } in
-      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; }
-
-let get_result r =
-  match r with
-  | Nonek -> None
-  | Somek (gls, fk) -> Some (gls.sigma,fk)
-
-let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals = 
-      if !typeclasses_dependency_order then
-	top_sort evm' goals
-      else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+         if !foundone == false && !typeclasses_debug > 0 then
+           Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++
+                        Printer.pr_constr_env (Goal.env gl) s concl ++
+                        spc () ++ str ", " ++ int (List.length poss) ++
+                        str" possibilities");
+         match e with
+         | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
+         | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx
     in
-    let res = run_list_tac tac p goals 
-      (make_autogoals ~only_classes ~unique ~st hints goals evm') in
-      match get_result res with
-      | None -> raise Not_found
-      | Some (evm', fk) -> 
-	Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk)
-
-let eauto_tac hints =
-  then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
-
-let eauto_tac ?limit hints =
-  if get_typeclasses_iterative_deepening () then
-    match limit with
-    | None -> fix_iterative (eauto_tac hints)
-    | Some limit -> fix_iterative_limit limit (eauto_tac hints)
-  else
-    match limit with
-    | None -> fix (eauto_tac hints)
-    | Some limit -> fix_limit limit (eauto_tac hints)
-
-let real_eauto ?limit unique st hints p evd =
-  let res =
-    run_on_evars ~st ~unique p evd hints (eauto_tac ?limit hints)
-  in
+    if backtrack then aux (NotApplicableEx,Exninfo.null) poss
+    else tclONCE (aux (NotApplicableEx,Exninfo.null) poss)
+
+  let hints_tac hints info kont : unit Proofview.tactic =
+    Proofview.Goal.nf_enter
+      { enter = fun gl -> hints_tac_gl hints info kont gl }
+
+  let intro_tac info kont gl =
+    let open Proofview in
+    let open Proofview.Notations in
+    let env = Goal.env gl in
+    let sigma = Goal.sigma gl in
+    let s = Sigma.to_evar_map sigma in
+    let decl = Tacmach.New.pf_last_hyp gl in
+    let hint =
+      make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
+                       (true,false,false) info.search_only_classes None decl in
+    let ldb = Hint_db.add_list env s hint info.search_hints in
+    let info' =
+      { info with search_hints = ldb; last_tac = lazy (str"intro") }
+    in kont info'
+
+  let intro info kont =
+    Proofview.tclBIND Tactics.intro
+     (fun _ -> Proofview.Goal.nf_enter { enter = fun gl -> intro_tac info kont gl })
+
+  let rec search_tac hints limit depth =
+    let kont info =
+      Proofview.numgoals >>= fun i ->
+      if !typeclasses_debug > 1 then
+        Feedback.msg_debug (str"calling eauto recursively at depth " ++ int (succ depth)
+                   ++ str" on " ++ int i ++ str" subgoals");
+      search_tac hints limit (succ depth) info
+    in
+    fun info ->
+    if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx
+    else
+      Proofview.tclOR (hints_tac hints info kont)
+                      (fun e -> Proofview.tclOR (intro info kont)
+                      (fun e' -> let (e, info) = merge_exceptions e e' in
+                              Proofview.tclZERO ~info e))
+
+  let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
+        unit Proofview.tactic =
+    let open Proofview in
+    let open Proofview.Notations in
+    let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+    search_tac hints depth 1 info
+
+  exception HasShelvedGoals
+
+  let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
+    let open Proofview in
+    let tac sigma gls i =
+      Goal.nf_enter
+        { enter = fun gl ->
+          search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl }
+    in
+      Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+      Proofview.tclEVARMAP >>= fun sigma ->
+      let j = List.length gls in
+      (tclDISPATCH (List.init j (fun i -> tac sigma gls i)))
+
+  let fix_iterative t =
+    let rec aux depth =
+      Proofview.tclOR (t depth)
+                      (function
+                       | (ReachedLimitEx,_) -> aux (succ depth)
+                       | (e,ie) -> Proofview.tclZERO ~info:ie e)
+    in aux 1
+
+  let fix_iterative_limit limit t =
+    let open Proofview in
+    let rec aux depth =
+      if Int.equal depth (succ limit) then tclZERO ReachedLimitEx
+      else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth)
+                                   | (e,ie) -> Proofview.tclZERO ~info:ie e)
+    in aux 1
+
+  let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints =
+    let tac =
+      let search = search_tac ~st only_classes dep hints in
+      if get_typeclasses_iterative_deepening () then
+        match depth with
+        | None -> fix_iterative search
+        | Some l -> fix_iterative_limit l search
+      else
+        let depth = match depth with None -> -1 | Some d -> d in
+        search depth
+    in
+    let error (e, ie) =
+      match e with
+      | ReachedLimitEx ->
+         Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
+      | NotApplicableEx ->
+         Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
+                                    (if Option.is_empty depth then mt()
+                                     else str" without reaching its limit"))
+      | e -> Proofview.tclZERO ~info:ie e
+    in Proofview.tclORELSE tac error
+
+  let run_on_evars ?(unique=false) p evm tac =
+    match evars_to_goals p evm with
+    | None -> None (* This happens only because there's no evar having p *)
+    | Some (goals, evm') ->
+       let goals =
+         if !typeclasses_dependency_order then
+           top_sort evm' goals
+         else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+       in
+       let fgoals = Evd.future_goals evm in
+       let pgoal = Evd.principal_future_goal evm in
+       let _, pv = Proofview.init evm' [] in
+       let pv = Proofview.unshelve goals pv in
+       try
+         let (), pv', (unsafe, shelved, gaveup), _ =
+           Proofview.apply (Global.env ()) tac pv
+         in
+         if Proofview.finished pv' then
+           let evm' = Proofview.return pv' in
+           assert(Evd.fold_undefined (fun ev _ acc ->
+                      let okev = Evd.mem evm ev || List.mem ev shelved in
+                      if not okev then
+                        Feedback.msg_debug
+                          (str "leaking evar " ++ int (Evar.repr ev) ++
+                             spc () ++ pr_ev evm' ev);
+                      acc && okev) evm' true);
+           let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in
+           let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
+           Some evm'
+         else raise Not_found
+       with Logic_monad.TacticFailure _ -> raise Not_found
+
+  let eauto depth only_classes unique dep st hints p evd =
+    let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in
+    let res = run_on_evars ~unique p evd eauto_tac in
     match res with
     | None -> evd
-    | Some (evd', fk) -> 
-      if unique then
-	(match get_result (fk NotApplicable) with
-	| Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions"
-	| None -> evd')
-      else evd'
-    
-let resolve_all_evars_once debug limit unique p evd =
-  let db = searchtable_map typeclasses_db in
-    real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd
-
-let eauto85 ?(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; } ->
-	{it = List.map fst goals; sigma = s;}
+    | Some evd' -> evd'
+  (* TODO treat unique solutions *)
+
+  let typeclasses_eauto ?depth unique st hints p evd =
+    eauto depth true unique false st hints p evd
+  (** Typeclasses eauto is an eauto which tries to resolve only
+      goals of typeclass type, and assumes that the initially selected
+      evars in evd are independent of the rest of the evars *)
+
+  let typeclasses_resolve debug depth unique p evd =
+    let db = searchtable_map typeclasses_db in
+    typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
+end
+
+(** Binding to either V85 or Search implementations. *)
+let eauto depth ~only_classes ~st ~dep dbs =
+  Search.eauto_tac ~st ~only_classes ~depth ~dep dbs
+
+let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
+                      ~depth dbs =
+  let dbs = List.map_filter
+              (fun db -> try Some (searchtable_map db)
+                      with e when Errors.noncritical e -> None)
+              dbs
+  in
+  let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+  let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
+  if get_typeclasses_compat () = Flags.V8_5 then
+    Tacticals.New.tclORELSE (Proofview.V82.tactic
+       (V85.eauto85 depth ~only_classes ~st dbs))
+     (Proofview.Goal.nf_enter ({ enter = fun gl ->
+       Tacticals.New.tclFAIL 0 (str" typeclasses eauto failed on: " ++
+                    Goal.pr_goal (Proofview.Goal.goal gl))}))
+  else eauto depth ~only_classes ~st ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
@@ -1256,24 +1286,6 @@ let evar_dependencies evm p =
       in Intpart.union_set evars p)
     evm ()
 
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
-  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' = eauto85 ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
-  let evd = sig_sig gls' 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_instantiation_problem := 
-    (fun x y z w -> resolve_one_typeclass x ~sigma:y z w)
-
 (** [split_evars] returns groups of undefined evars according to dependencies *)
 
 let split_evars evm =
@@ -1289,9 +1301,9 @@ let is_inference_forced p evd ev =
     then
       let (loc, k) = evar_source ev evd in
       match k with
-	| Evar_kinds.ImplicitArg (_, _, b) -> b
-	| Evar_kinds.QuestionMark _ -> false
-	| _ -> true
+        | Evar_kinds.ImplicitArg (_, _, b) -> b
+        | Evar_kinds.QuestionMark _ -> false
+        | _ -> true
     else true
   with Not_found -> assert false
 
@@ -1358,12 +1370,11 @@ let revert_resolvability oevd evd =
   in
   Evd.raw_map_undefined map evd
 
-(** 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 unique env p oevd do_split fail =
+(** If [do_split] is [true], we try to separate the problem in
+    several components and then solve them separately *)
+let resolve_all_evars debug depth unique env p oevd do_split fail =
   let split = if do_split then split_evars oevd else [Evar.Set.empty] in
   let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
   in
@@ -1372,20 +1383,20 @@ let resolve_all_evars debug m unique env p oevd do_split fail =
     | comp :: comps ->
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
-	let evd' =
+        let evd' =
           if get_typeclasses_compat () = Flags.Current then
-            resolve_all_evars_once' debug m unique p evd
-          else resolve_all_evars_once debug m unique p evd
+            Search.typeclasses_resolve debug depth unique p evd
+          else V85.resolve_all_evars_once debug depth unique p evd
         in
-	 if has_undefined p oevd evd' then raise Unresolved;
-	 docomp evd' comps
+         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. *)
+        if fail && (not do_split || is_mandatory (p evd) comp evd)
+        then (* Unable to satisfy the constraints. *)
           let comp = if do_split then Some comp else None in
-	  error_unresolvable env comp evd
-	else (* Best effort: do nothing on this component *)
-	  docomp evd comps
+          error_unresolvable env comp evd
+        else (* Best effort: do nothing on this component *)
+          docomp evd comps
   in docomp oevd split
 
 let initial_select_evars filter =
@@ -1393,13 +1404,14 @@ let initial_select_evars filter =
     filter ev (snd evi.Evd.evar_source) &&
     Typeclasses.is_class_evar evd evi
 
-let resolve_typeclass_evars debug m unique env evd filter split fail =
+let resolve_typeclass_evars debug depth unique env evd filter split fail =
   let evd =
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with e when Errors.noncritical e -> evd
   in
-    resolve_all_evars debug m unique env (initial_select_evars filter) evd split fail
+    resolve_all_evars debug depth unique env
+                      (initial_select_evars filter) evd split fail
 
 let solve_inst env evd filter unique split fail =
   resolve_typeclass_evars
@@ -1410,22 +1422,24 @@ let solve_inst env evd filter unique split fail =
 let _ =
   Typeclasses.solve_instantiations_problem := solve_inst
 
-let eauto ?limit ~only_classes ~st dbs =
-  new_eauto_tac ~st only_classes ?limit dbs
-
-let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs =
-  let dbs = List.map_filter
-              (fun db -> try Some (searchtable_map db)
-                      with e when Errors.noncritical e -> None)
-              dbs
+let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
+  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' = V85.eauto85 !typeclasses_depth
+                         ~st:(Hint_db.transparent_state hints) [hints] gls in
+  let evd = sig_sig gls' in
+  let t' = let (ev, inst) = destEvar t in
+    mkEvar (ev, Array.of_list subst)
   in
-  let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
-  if get_typeclasses_compat () = Flags.V8_5 then
-    Tacticals.New.tclORELSE (Proofview.V82.tactic (eauto85 ?limit:!typeclasses_depth ~only_classes ~st dbs))
-     (Proofview.Goal.nf_enter ({ enter = fun gl ->
-       Tacticals.New.tclFAIL 0 (str" typeclasses eauto failed on: " ++
-                    Goal.pr_goal (Proofview.Goal.goal gl))}))
-  else eauto ?limit:!typeclasses_depth ~only_classes ~st true dbs
+  let term = Evarutil.nf_evar evd t' in
+    evd, term
+
+let _ =
+  Typeclasses.solve_instantiation_problem :=
+    (fun x y z w -> resolve_one_typeclass x ~sigma:y z w)
 
 (** Take the head of the arity of a constr.
     Used in the partial application tactic. *)
@@ -1449,11 +1463,3 @@ let not_evar c = match kind_of_term c with
 let is_ground c gl =
   if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
   else tclFAIL 0 (str"Not ground") gl
-
-let autoapply c i gl =
-  let flags = auto_unif_flags Evar.Set.empty 
-    (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_unsafe_type_of gl c in
-  let ce = mk_clenv_from gl (c,cty) in
-  let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),None,ce) } in
-  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 48abba1aa..2fb0bbb04 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -20,10 +20,9 @@ val get_typeclasses_debug : unit -> bool
 val set_typeclasses_depth : int option -> unit
 val get_typeclasses_depth : unit -> int option
 
-val progress_evars : unit Proofview.tactic -> unit Proofview.tactic
-
 val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
-  Hints.hint_db_name list -> unit Proofview.tactic
+                        depth:(Int.t option) ->
+                        Hints.hint_db_name list -> unit Proofview.tactic
 
 val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic
 
@@ -33,24 +32,18 @@ val is_ground : constr -> tactic
 
 val autoapply : constr -> Hints.hint_db_name -> tactic
        
-type newautoinfo =
-  { search_depth : int list;
-    last_tac : Pp.std_ppcmds Lazy.t;
-    search_dep : bool;
-    search_cut : Hints.hints_path;
-    search_hints : Hints.Hint_db.t }
-
-val new_hints_tac : bool -> Hints.hint_db list ->
-                    newautoinfo ->
-                    (newautoinfo -> unit Proofview.tactic) -> unit Proofview.tactic
-
-val make_autogoal' : ?st:Names.transparent_state ->
-           bool -> bool ->
-           Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo
-
-val new_eauto_tac : ?st:Names.transparent_state ->
-  bool -> ?limit:Int.t ->
-  bool -> (* Should the tactic be made backtracking, whatever the dependencies
-            betwwen initial goals are *)
-  Hints.hint_db list -> unit Proofview.tactic
-
+module Search : sig
+  val eauto_tac :
+    ?st:Names.transparent_state ->
+    (** The transparent_state used when working with local hypotheses  *)
+    only_classes:bool ->
+    (** Should non-class goals be shelved and resolved at the end *)
+    depth:Int.t option ->
+    (** Bounded or unbounded search *)
+    dep:bool ->
+    (** Should the tactic be made backtracking on the initial goals, 
+       whatever their internal dependencies are. *)
+    Hints.hint_db list ->
+    (** The list of hint databases to use *)
+    unit Proofview.tactic
+end
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 8d6cbfcde..dfa438d90 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -18,6 +18,7 @@ Goal exists R, @Refl nat R.
   Set Typeclasses Debug.
   (* Fail solve [unshelve eauto with foo]. *)
   Set Typeclasses Debug Verbosity 1.
+  Test Typeclasses Depth.
   solve [typeclasses eauto with foo].
 Qed.
 
@@ -117,15 +118,14 @@ Module IterativeDeepening.
   Goal C -> A.
     intros.
     Set Typeclasses Debug.
-    Fail Timeout 1 fulleauto.
+    Fail Timeout 1 typeclasses eauto.
     Set Typeclasses Iterative Deepening.
-    Fail fulleauto 1.
-    fulleauto 2.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
     Undo.
     Unset Typeclasses Iterative Deepening.
     Fail Timeout 1 typeclasses eauto.
     Set Typeclasses Iterative Deepening.
-    Typeclasses eauto := 3.
     typeclasses eauto.
   Qed.
 
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index f55e32032..eadba47b8 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -38,3 +38,69 @@ Goal exists n, n = 42.
   (* Does backtrack between individual goals *)
   all:(typeclasses eauto).
 Qed.
+
+Fail Timeout 1 Check prf.
+
+Hint Mode SomeProp + + : typeclass_instances.
+Check prf.
+Check (fun H : SomeProp plus => _ : SomeProp (flip plus)).
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+(** Iterative deepening / breadth-first search *)
+
+Module IterativeDeepening.
+
+  Class A.
+  Class B.
+  Class C.
+
+  Instance: B -> A | 0.
+  Instance: C -> A | 0.
+  Instance: C -> B -> A | 0.
+  Instance: A -> A | 0.
+  
+  Goal C -> A.
+    intros.
+    Set Typeclasses Debug.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
+    Undo.
+    Unset Typeclasses Iterative Deepening.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Typeclasses eauto := debug 3.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 17b3aaef2..c9c7c611c 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -16,30 +16,30 @@ Instance bn1: B nat 1.
 
 Goal A nat.
 Proof.
-  fulleauto.
+  typeclasses eauto.
 Qed.
 
 Goal B nat 2.
 Proof.
-  Fail fulleauto.
+  Fail typeclasses eauto.
 Abort.
 
 Goal exists T : Type, A T.
 Proof.
-  eexists. fulleauto.
+  eexists. typeclasses eauto.
 Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
-  eexists. eexists. fulleauto.
+  eexists. eexists. typeclasses eauto.
 Defined.
 
 Instance ab: A bool. (* Backtrack on A instance *)
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
-  eexists. eexists. fulleauto.
+  eexists. eexists. typeclasses eauto.
 Defined.
 
 Class C {T} `(a : A T) (t : T). 
@@ -52,14 +52,14 @@ Instance can: C an 0.
 (* Backtrack on instance implementation *)
 Goal exists (T : Type) (t : T), { x : A T & C x t }.
 Proof.
-  eexists. eexists. fulleauto.
+  eexists. eexists. typeclasses eauto.
 Defined.
 
 Class D T `(a: A T).
   Instance: D _ an.
 Goal exists (T : Type), { x : A T & D T x }.
 Proof.
-  eexists. fulleauto.
+  eexists. typeclasses eauto.
 Defined.
   
 
@@ -115,11 +115,11 @@ Lemma simpl_plus_l_rr1 :
   apply H0. apply f_equal_nat.
   Time info_eauto.
   Undo.
-  Unset Typeclasses Debug.
+  Set Typeclasses Debug.
   Set Typeclasses Iterative Deepening.
-  Time fulleauto 5. Show Proof.
+  Time typeclasses eauto 2 with nocore. Show Proof.
   Undo.
-  eauto. (* does EApply H *)
+  Time eauto. (* does EApply H *)
 Qed.
 
 (* Example from Nicolas Tabareau on coq-club - Feb 2016. 
@@ -155,10 +155,11 @@ Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
 Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instances.
 
+Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time fulleauto 10.
+  Time typeclasses eauto 10.
   Undo. Set Typeclasses Iterative Deepening.
-  Time fulleauto.
+  Time typeclasses eauto.
 Defined.