Moving Eauto and Class_tactics to tactics/.

5 files changed, 1496 insertions, 0 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
new file mode 100644
index 0000000000..4855598989
--- /dev/null
+++ b/tactics/class_tactics.ml
@@ -0,0 +1,903 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Termops
+open Reduction
+open Proof_type
+open Tacticals
+open Tacmach
+open Tactics
+open Clenv
+open Typeclasses
+open Globnames
+open Evd
+open Locus
+open Misctypes
+open Proofview.Notations
+open Hints
+
+(** Hint database named "typeclass_instances", now created directly in Auto *)
+
+let typeclasses_debug = ref false
+let typeclasses_depth = ref None
+
+let typeclasses_modulo_eta = ref false
+let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d
+let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta
+
+let typeclasses_dependency_order = ref false
+let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d
+let get_typeclasses_dependency_order () = !typeclasses_dependency_order
+
+let typeclasses_iterative_deepening = ref false
+let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d
+let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "do typeclass search modulo eta conversion";
+      optkey   = ["Typeclasses";"Modulo";"Eta"];
+      optread  = get_typeclasses_modulo_eta;
+      optwrite = set_typeclasses_modulo_eta; }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "during typeclass resolution, solve instances according to their dependency order";
+      optkey   = ["Typeclasses";"Dependency";"Order"];
+      optread  = get_typeclasses_dependency_order;
+      optwrite = set_typeclasses_dependency_order; }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "use iterative deepening strategy";
+      optkey   = ["Typeclasses";"Iterative";"Deepening"];
+      optread  = get_typeclasses_iterative_deepening;
+      optwrite = set_typeclasses_iterative_deepening; }
+
+(** 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)
+
+(** Typeclasses instance search tactic / eauto *)
+
+open Auto
+
+open Unification
+
+let auto_core_unif_flags st freeze = {
+  modulo_conv_on_closed_terms = Some st;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
+  modulo_delta = st;
+  modulo_delta_types = st;
+  check_applied_meta_types = false;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = freeze;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = true;
+  modulo_eta = !typeclasses_modulo_eta;
+}
+
+let auto_unif_flags freeze st = 
+  let fl = auto_core_unif_flags st freeze in
+  { core_unify_flags = fl;
+    merge_unify_flags = fl;
+    subterm_unify_flags = fl;
+    allow_K_in_toplevel_higher_order_unification = false;
+    resolve_evars = false
+}
+
+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 =
+    if poly then
+      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}
+    else c, gl
+  in
+  let t1 = pf_unsafe_type_of gl c in
+    tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
+
+let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) ->
+  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv'
+  end }
+
+let unify_resolve poly flags = { enter = begin fun gls (c,clenv) ->
+  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv'
+  end }
+
+let clenv_of_prods poly nprods (c, clenv) gl =
+  let (c, _, _) = c in
+  if poly || Int.equal nprods 0 then Some clenv
+  else
+    let ty = Tacmach.New.pf_unsafe_type_of gl c in
+    let diff = nb_prod ty - nprods in
+      if Pervasives.(>=) diff 0 then
+        (* Was Some clenv... *)
+	Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
+      else None
+
+let with_prods nprods poly (c, clenv) f =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  match clenv_of_prods poly nprods (c, clenv) gl with
+  | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+  | Some clenv' -> f.enter gl (c, clenv')
+  end }
+
+(** Hack to properly solve dependent evars that are typeclasses *)
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl =
+    Proofview.V82.of_tactic Eauto.registered_e_assumption ::
+    (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	      (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
+    (List.map (fun (x,_,_,_,_) -> x) 
+     (e_trivial_resolve db_list local_db (project goal) (pf_concl goal)))
+  in
+  tclFIRST (List.map tclCOMPLETE tacl) goal
+
+and e_my_find_search db_list local_db hdc complete sigma concl =
+  let prods, concl = decompose_prod_assum concl in
+  let nprods = List.length prods in
+  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
+    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)
+      (local_db::db_list)
+  in
+  let tac_of_hint =
+    fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
+      let tac = function
+      | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+      | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
+      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+         Proofview.V82.tactic (tclTHEN
+				 (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
+				 (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c])))
+      | Extern tacast -> conclPattern concl p tacast
+      in
+      let tac = Proofview.V82.of_tactic (run_hint t tac) in
+      let tac = if complete then tclCOMPLETE tac else tac in
+	match repr_hint t with
+	| Extern _ -> (tac,b,true, name, lazy (pr_hint t))
+	| _ ->
+(* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
+	    (tac,b,false, name, lazy (pr_hint t))
+  in List.map tac_of_hint hintl
+
+and e_trivial_resolve db_list local_db sigma concl =
+  try
+    e_my_find_search db_list local_db
+     (decompose_app_bound concl) true sigma concl
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db sigma concl =
+  try
+    e_my_find_search db_list local_db
+      (decompose_app_bound concl) false sigma concl
+  with Bound | Not_found -> []
+
+let catchable = function
+  | Refiner.FailError _ -> true
+  | e -> Logic.catchable_exception e
+
+let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
+
+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
+
+type atac = auto_result tac
+
+(* Some utility types to avoid the need of -rectypes *)
+
+type 'a optionk =
+  | Nonek
+  | Somek of 'a * 'a optionk fk
+
+type ('a,'b) optionk2 =
+  | Nonek2 of failure
+  | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+
+let make_resolve_hyp env sigma st flags only_classes pri decl =
+  let open Context.Named.Declaration in
+  let id = get_id decl in
+  let cty = Evarutil.nf_evar sigma (get_type decl) in
+  let rec iscl env ty =
+    let ctx, ar = decompose_prod_assum ty in
+      match kind_of_term (fst (decompose_app ar)) with
+      | 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
+  in
+  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 (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])
+    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 =
+    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
+  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 }
+
+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
+
+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
+
+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 =
+  { 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 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 (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 then
+	      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 then
+		    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 then
+	  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 cut_of_hints h =
+  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+
+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)
+    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
+    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 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; } ->
+	{it = List.map fst goals; sigma = s;}
+
+(** 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(Evar.Set)(Evar.Map)
+
+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 (Evar.Set.union evx evy) p)
+    cstrs
+
+let evar_dependencies evm p =
+  Evd.fold_undefined
+    (fun ev evi _ ->
+      let evars = Evar.Set.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 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' = eauto ?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 =
+  let p = Intpart.create () in
+  evar_dependencies evm p;
+  deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
+  Intpart.partition p
+
+let is_inference_forced p evd ev =
+  try
+    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
+	| Evar_kinds.ImplicitArg (_, _, b) -> b
+	| Evar_kinds.QuestionMark _ -> false
+	| _ -> true
+    else true
+  with Not_found -> assert false
+
+let is_mandatory p comp evd =
+  Evar.Set.exists (is_inference_forced p evd) comp
+
+(** In case of unsatisfiable constraints, build a nice error message *)
+
+let error_unresolvable env comp evd =
+  let evd = Evarutil.nf_evar_map_undefined evd in
+  let is_part ev = match comp with
+  | None -> true
+  | Some s -> Evar.Set.mem ev s
+  in
+  let fold ev evi (found, accu) =
+    let ev_class = class_of_constr evi.evar_concl in
+    if not (Option.is_empty ev_class) && is_part ev then
+      (* focus on one instance if only one was searched for *)
+      if not found then (true, Some ev)
+      else (found, None)
+    else (found, accu)
+   in
+  let (_, ev) = Evd.fold_undefined fold evd (true, None) in
+    Pretype_errors.unsatisfiable_constraints
+      (Evarutil.nf_env_evar evd env) evd ev comp
+
+(** 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 =
+  let check ev evi = snd (p oevd ev evi) in
+  Evar.Map.exists check (Evd.undefined_map evd)
+
+(** Revert the resolvability status of evars after resolution,
+    potentially unprotecting some evars that were set unresolvable
+    just for this call to resolution. *)
+
+let revert_resolvability oevd evd =
+  let map ev evi =
+    try
+      if not (Typeclasses.is_resolvable evi) then
+        let evi' = Evd.find_undefined oevd ev in
+        if Typeclasses.is_resolvable evi' then
+          Typeclasses.mark_resolvable evi
+        else evi
+      else evi
+    with Not_found -> evi
+  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 =
+  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
+  let rec docomp evd = function
+    | [] -> revert_resolvability oevd evd
+    | comp :: comps ->
+      let p = select_and_update_evars p oevd (in_comp comp) in
+      try
+	 let evd' = resolve_all_evars_once debug m unique 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. *)
+          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
+  in docomp oevd split
+
+let initial_select_evars filter =
+  fun evd ev evi ->
+    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 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
+
+let solve_inst debug depth env evd filter unique split fail =
+  resolve_typeclass_evars debug depth unique env evd filter split fail
+
+let _ =
+  Typeclasses.solve_instantiations_problem :=
+    solve_inst false !typeclasses_depth
+
+let set_typeclasses_debug d = (:=) typeclasses_debug d;
+  Typeclasses.solve_instantiations_problem := solve_inst d !typeclasses_depth
+
+let get_typeclasses_debug () = !typeclasses_debug
+
+let set_typeclasses_depth d = (:=) typeclasses_depth d;
+  Typeclasses.solve_instantiations_problem := solve_inst !typeclasses_debug !typeclasses_depth
+
+let get_typeclasses_depth () = !typeclasses_depth
+
+open Goptions
+
+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 =
+  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 typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
+  try
+    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
+      eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
+   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
+
+(** Take the head of the arity of a constr.
+    Used in the partial application tactic. *)
+
+let rec head_of_constr t =
+  let t = strip_outer_cast(collapse_appl t) in
+    match kind_of_term t with
+    | Prod (_,_,c2)  -> head_of_constr c2
+    | LetIn (_,_,_,c2) -> head_of_constr c2
+    | App (f,args)  -> head_of_constr f
+    | _      -> t
+
+let head_of_constr h c =
+  let c = head_of_constr c in
+  letin_tac None (Name h) c None Locusops.allHyps
+
+let not_evar c = match kind_of_term c with
+| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+| _ -> Proofview.tclUNIT ()
+
+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),ce) } in
+  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
new file mode 100644
index 0000000000..f1bcfa7dd4
--- /dev/null
+++ b/tactics/class_tactics.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Constr
+open Tacmach
+
+val catchable : exn -> bool
+
+val set_typeclasses_debug : bool -> unit
+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 -> tactic
+
+val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic
+
+val not_evar : constr -> unit Proofview.tactic
+
+val is_ground : constr -> tactic
+
+val autoapply : constr -> Hints.hint_db_name -> tactic
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
new file mode 100644
index 0000000000..9cfb805d4c
--- /dev/null
+++ b/tactics/eauto.ml
@@ -0,0 +1,526 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Proof_type
+open Tacticals
+open Tacmach
+open Tactics
+open Patternops
+open Clenv
+open Auto
+open Genredexpr
+open Tacexpr
+open Misctypes
+open Locus
+open Locusops
+open Hints
+open Proofview.Notations
+
+let eauto_unif_flags = auto_flags_of_state full_transparent_state
+
+let e_give_exact ?(flags=eauto_unif_flags) c =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+  let t2 = Tacmach.New.pf_concl gl in
+  if occur_existential t1 || occur_existential t2 then
+     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+  else exact_check c
+  end }
+
+let assumption id = e_give_exact (mkVar id)
+
+let e_assumption =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
+  end }
+
+let registered_e_assumption =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+              (Tacmach.New.pf_ids_of_hyps gl))
+  end }
+
+let eval_uconstrs ist cs =
+  let flags = {
+    Pretyping.use_typeclasses = false;
+    use_unif_heuristics = true;
+    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    fail_evar = false;
+    expand_evars = true
+  } in
+  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
+
+(************************************************************************)
+(*   PROLOG tactic                                                      *)
+(************************************************************************)
+
+(*s Tactics handling a list of goals. *)
+
+(* first_goal : goal list sigma -> goal sigma *)
+
+let first_goal gls =
+  let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
+  if List.is_empty gl then error "first_goal";
+  { Evd.it = List.hd gl; Evd.sigma = sig_0; }
+
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+let apply_tac_list tac glls =
+  let (sigr,lg) = unpackage glls in
+  match lg with
+  | (g1::rest) ->
+      let gl = apply_sig_tac sigr tac g1 in
+      repackage sigr (gl@rest)
+  | _ -> error "apply_tac_list"
+
+let one_step l gl =
+  [Proofview.V82.of_tactic Tactics.intro]
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
+  @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
+
+let rec prolog l n gl =
+  if n <= 0 then error "prolog - failure";
+  let prol = (prolog l (n-1)) in
+  (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
+
+let out_term = function
+  | IsConstr (c, _) -> c
+  | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
+
+let prolog_tac l n =
+  Proofview.V82.tactic begin fun gl ->
+  let map c =
+    let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
+    let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
+    out_term c
+  in
+  let l = List.map map l in
+  try (prolog l n gl)
+  with UserError ("Refiner.tclFIRST",_) ->
+    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+  end
+
+open Auto
+open Unification
+
+(***************************************************************************)
+(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
+(***************************************************************************)
+
+let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
+			  
+let unify_e_resolve poly flags (c,clenv) =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let clenv', c = connect_hint_clenv poly c clenv gl in
+      Proofview.V82.tactic
+	(fun gls ->
+	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
+	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+    end }
+
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none db
+  | Some hdc ->
+    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
+    else (fun db -> Hint_db.map_auto hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
+let e_exact poly flags (c,clenv) =
+  let (c, _, _) = c in
+  let clenv', subst = 
+    if poly then Clenv.refresh_undefined_univs clenv 
+    else clenv, Univ.empty_level_subst
+  in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
+
+let rec e_trivial_fail_db db_list local_db =
+  let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let d = Tacmach.New.pf_last_hyp gl in
+    let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
+    e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
+  end } in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let tacl =
+    registered_e_assumption ::
+    (Tacticals.New.tclTHEN Tactics.intro next) ::
+    (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
+  in
+  Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
+  end }
+
+and e_my_find_search db_list local_db hdc concl =
+  let hint_of_db = hintmap_of hdc concl in
+  let hintl =
+      List.map_append (fun db ->
+	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
+	  List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
+  in
+  let tac_of_hint =
+    fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
+      let b = match Hints.repr_hint t with
+      | Unfold_nth _ -> 1
+      | _ -> b
+      in
+      (b,
+        let tac = function
+        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
+        | Give_exact (c,cl) -> e_exact poly st (c,cl)
+        | Res_pf_THEN_trivial_fail (term,cl) ->
+          Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
+            (e_trivial_fail_db db_list local_db)
+        | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
+        | Extern tacast -> conclPattern concl p tacast
+       in
+       let tac = run_hint t tac in
+       (tac, lazy (pr_hint t)))
+  in
+  List.map tac_of_hint hintl
+
+and e_trivial_resolve db_list local_db gl =
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try priority (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
+
+let find_first_goal gls =
+  try first_goal gls with UserError _ -> assert false
+
+(*s The following module [SearchProblem] is used to instantiate the generic
+    exploration functor [Explore.Make]. *)
+
+type search_state = {
+  priority : int;
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma;
+  last_tactic : std_ppcmds Lazy.t;
+  dblist : hint_db list;
+  localdb :  hint_db list;
+  prev : prev_search_state;
+  local_lemmas : Tacexpr.delayed_open_constr list;
+}
+
+and prev_search_state = (* for info eauto *)
+  | Unknown
+  | Init
+  | State of search_state
+
+module SearchProblem = struct
+
+  type state = search_state
+
+  let success s = List.is_empty (sig_it s.tacres)
+
+(*   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *)
+
+  let filter_tactics glls l =
+(*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+(*     let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
+    let rec aux = function
+      | [] -> []
+      | (tac, cost, pptac) :: tacl ->
+	  try
+	    let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
+(* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+(* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
+	      (lgls, cost, pptac) :: aux tacl
+	  with e when Errors.noncritical e ->
+            let e = Errors.push e in
+            Refiner.catch_failerror e; aux tacl
+    in aux l
+
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
+  let compare s s' =
+    let d = s'.depth - s.depth in
+    let d' = Int.compare s.priority s'.priority in
+    let nbgoals s = List.length (sig_it s.tacres) in
+    if not (Int.equal d 0) then d
+    else if not (Int.equal d' 0) then d'
+    else Int.compare (nbgoals s) (nbgoals s')
+
+  let branching s =
+    if Int.equal s.depth 0 then
+      []
+    else
+      let ps = if s.prev == Unknown then Unknown else State s in
+      let lg = s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+      let assumption_tacs =
+        let tacs = List.map map_assum (pf_ids_of_hyps g) in
+        let l = filter_tactics s.tacres tacs in
+	List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
+				    last_tactic = pp; dblist = s.dblist;
+				    localdb = List.tl s.localdb;
+				    prev = ps; local_lemmas = s.local_lemmas}) l
+      in
+      let intro_tac =
+        let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
+	List.map
+	  (fun (lgls, cost, pp) ->
+	     let g' = first_goal lgls in
+	     let hintl =
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list (pf_env g') (project g')
+		  hintl (List.hd s.localdb) in
+	     { depth = s.depth; priority = cost; tacres = lgls;
+	       last_tactic = pp; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb; prev = ps;
+               local_lemmas = s.local_lemmas})
+	  l
+      in
+      let rec_tacs =
+	let l =
+	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map
+	  (fun (lgls, cost, pp) ->
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
+                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
+                  local_lemmas = s.local_lemmas }
+	     else
+	       let newlocal = 
+		 let hyps = pf_hyps g in
+		   List.map (fun gl ->
+		     let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
+		     let hyps' = pf_hyps gls in
+		       if hyps' == hyps then List.hd s.localdb
+		       else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas)
+		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
+	       in
+		 { depth = pred s.depth; priority = cost; tacres = lgls;
+		   dblist = s.dblist; last_tactic = pp; prev = ps;
+		   localdb = newlocal @ List.tl s.localdb;
+                   local_lemmas = s.local_lemmas })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
+		      (Lazy.force s.last_tactic))
+
+end
+
+module Search = Explore.Make(SearchProblem)
+
+(** Utilities for debug eauto / info eauto *)
+
+let global_debug_eauto = ref false
+let global_info_eauto = ref false
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Debug Eauto";
+      Goptions.optkey   = ["Debug";"Eauto"];
+      Goptions.optread  = (fun () -> !global_debug_eauto);
+      Goptions.optwrite = (:=) global_debug_eauto }
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Info Eauto";
+      Goptions.optkey   = ["Info";"Eauto"];
+      Goptions.optread  = (fun () -> !global_info_eauto);
+      Goptions.optwrite = (:=) global_info_eauto }
+
+let mk_eauto_dbg d =
+  if d == Debug || !global_debug_eauto then Debug
+  else if d == Info || !global_info_eauto then Info
+  else Off
+
+let pr_info_nop = function
+  | Info -> msg_debug (str "idtac.")
+  | _ -> ()
+
+let pr_dbg_header = function
+  | Off -> ()
+  | Debug -> msg_debug (str "(* debug eauto : *)")
+  | Info -> msg_debug (str "(* info eauto : *)")
+
+let pr_info dbg s =
+  if dbg != Info then ()
+  else
+    let rec loop s =
+      match s.prev with
+	| Unknown | Init -> s.depth
+	| State sp ->
+	  let mindepth = loop sp in
+	  let indent = String.make (mindepth - sp.depth) ' ' in
+	  msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+	  mindepth
+    in
+    ignore (loop s)
+
+(** Eauto main code *)
+
+let make_initial_state dbg n gl dblist localdb lems =
+  { depth = n;
+    priority = 0;
+    tacres = tclIDTAC gl;
+    last_tactic = lazy (mt());
+    dblist = dblist;
+    localdb = [localdb];
+    prev = if dbg == Info then Init else Unknown;
+    local_lemmas = lems;
+  }
+
+let e_search_auto debug (in_depth,p) lems db_list gl =
+  let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in
+  let d = mk_eauto_dbg debug in
+  let tac = match in_depth,d with
+    | (true,Debug) -> Search.debug_depth_first
+    | (true,_) -> Search.depth_first
+    | (false,Debug) -> Search.debug_breadth_first
+    | (false,_) -> Search.breadth_first
+  in
+  try
+    pr_dbg_header d;
+    let s = tac (make_initial_state d p gl db_list local_db lems) in
+    pr_info d s;
+    s.tacres
+  with Not_found ->
+    pr_info_nop d;
+    error "eauto: search failed"
+
+(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
+(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
+
+let eauto_with_bases ?(debug=Off) np lems db_list =
+  tclTRY (e_search_auto debug np lems db_list)
+
+let eauto ?(debug=Off) np lems dbnames =
+  let db_list = make_db_list dbnames in
+  tclTRY (e_search_auto debug np lems db_list)
+
+let full_eauto ?(debug=Off) n lems gl =
+  let dbnames = current_db_names () in
+  let dbnames =  String.Set.remove "v62" dbnames in
+  let db_list = List.map searchtable_map (String.Set.elements dbnames) in
+  tclTRY (e_search_auto debug n lems db_list) gl
+
+let gen_eauto ?(debug=Off) np lems = function
+  | None -> Proofview.V82.tactic (full_eauto ~debug np lems)
+  | Some l -> Proofview.V82.tactic (eauto ~debug np lems l)
+
+let make_depth = function
+  | None -> !default_search_depth
+  | Some d -> d
+
+let make_dimension n = function
+  | None -> (true,make_depth n)
+  | Some d -> (false,d)
+
+let cons a l = a :: l
+
+let autounfolds db occs cls gl =
+  let unfolds = List.concat (List.map (fun dbname -> 
+    let db = try searchtable_map dbname 
+      with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+    in
+    let (ids, csts) = Hint_db.unfolds db in
+    let hyps = pf_ids_of_hyps gl in
+    let ids = Idset.filter (fun id -> List.mem id hyps) ids in
+      Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
+	(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
+  in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
+
+let autounfold db cls =
+  Proofview.V82.tactic begin fun gl ->
+  let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
+  let tac = autounfolds db in
+  tclMAP (function
+    | OnHyp (id,occs,where) -> tac occs (Some (id,where))
+    | OnConcl occs -> tac occs None)
+    cls gl
+  end
+
+let autounfold_tac db cls =
+  Proofview.tclUNIT () >>= fun () ->
+  let dbs = match db with
+  | None -> String.Set.elements (current_db_names ())
+  | Some [] -> ["core"]
+  | Some l -> l
+  in
+  autounfold dbs cls
+
+let unfold_head env (ids, csts) c = 
+  let rec aux c = 
+    match kind_of_term c with
+    | Var id when Id.Set.mem id ids ->
+	(match Environ.named_body id env with
+	| Some b -> true, b
+	| None -> false, c)
+    | Const (cst,u as c) when Cset.mem cst csts ->
+	true, Environ.constant_value_in env c
+    | App (f, args) ->
+	(match aux f with
+	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+	| false, _ -> 
+	    let done_, args' = 
+	      Array.fold_left_i (fun i (done_, acc) arg -> 
+		if done_ then done_, arg :: acc 
+		else match aux arg with
+		| true, arg' -> true, arg' :: acc
+		| false, arg' -> false, arg :: acc)
+		(false, []) args
+	    in 
+	      if done_ then true, mkApp (f, Array.of_list (List.rev args'))
+	      else false, c)
+    | _ -> 
+	let done_ = ref false in
+	let c' = map_constr (fun c -> 
+	  if !done_ then c else 
+	    let x, c' = aux c in
+	      done_ := x; c') c
+	in !done_, c'
+  in aux c
+
+let autounfold_one db cl =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
+  let st =
+    List.fold_left (fun (i,c) dbname -> 
+      let db = try searchtable_map dbname 
+	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+      in
+      let (ids, csts) = Hint_db.unfolds db in
+	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
+  in
+  let did, c' = unfold_head env st 
+    (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
+  in
+    if did then
+      match cl with
+      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
+      | None -> convert_concl_no_check c' DEFAULTcast
+    else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+  end }
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
new file mode 100644
index 0000000000..8812093d5f
--- /dev/null
+++ b/tactics/eauto.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Proof_type
+open Hints
+
+val e_assumption : unit Proofview.tactic
+
+val registered_e_assumption : unit Proofview.tactic
+
+val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
+
+val prolog_tac : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic
+
+val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list ->
+  hint_db_name list option -> unit Proofview.tactic
+
+val eauto_with_bases :
+  ?debug:Tacexpr.debug ->
+  bool * int ->
+  Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic
+
+val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic
+val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic
+val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
+
+val make_dimension : int option -> int option -> bool * int
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index cb327e52c1..bbad1d8e64 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -17,5 +17,7 @@ Leminv
 Taccoerce
 Hints
 Auto
+Eauto
+Class_tactics
 Tactic_matching
 Term_dnet