Merge branch 'master'.

11 files changed, 391 insertions, 201 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c8c119aee1..74cb7a364f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -261,7 +261,7 @@ and erase_subtree depth = function
   | (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
 
 let pr_info_atom (d,pp) =
-  str (String.make d ' ') ++ pp () ++ str "."
+  str (String.make (d-1) ' ') ++ pp () ++ str "."
 
 let pr_info_trace = function
   | (Info,_,{contents=(d,Some pp)::l}) ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index b0ecb4660b..32710e3470 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -52,17 +52,15 @@ val new_auto : ?debug:debug ->
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : unit Proofview.tactic
 
-(** auto with all hint databases except the "v62" compatibility database *)
+(** auto with all hint databases *)
 val full_auto : ?debug:debug ->
   int -> delayed_open_constr list -> unit Proofview.tactic
 
-(** auto with all hint databases except the "v62" compatibility database
-   and doing delta *)
+(** auto with all hint databases and doing delta *)
 val new_full_auto : ?debug:debug ->
   int -> delayed_open_constr list -> unit Proofview.tactic
 
-(** auto with default search depth and with all hint databases
-   except the "v62" compatibility database *)
+(** auto with default search depth and with all hint databases *)
 val default_full_auto : unit Proofview.tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8bbef39ad5..64d76360ff 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -9,7 +9,6 @@
 (* TODO:
   - Find an interface allowing eauto to backtrack when shelved goals remain,
    e.g. to force instantiations.
-  - unique solutions
  *)
 
 open Pp
@@ -96,7 +95,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "do typeclass search modulo eta conversion";
       optkey   = ["Typeclasses";"Modulo";"Eta"];
       optread  = get_typeclasses_modulo_eta;
@@ -184,6 +183,12 @@ let set_typeclasses_depth =
       optread  = get_typeclasses_depth;
       optwrite = set_typeclasses_depth; }
 
+type search_strategy = Dfs | Bfs
+
+let set_typeclasses_strategy = function
+  | Dfs -> set_typeclasses_iterative_deepening false
+  | Bfs -> set_typeclasses_iterative_deepening true
+
 let pr_ev evs ev =
   Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev)
 
@@ -242,12 +247,11 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   end }
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags =
+let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
   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 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 =
         if poly then
@@ -262,15 +266,20 @@ let unify_resolve_refine poly flags =
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
       let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
-        let evdref = ref sigma' in
-        if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
-                                      evdref cl.cl_concl concl) then
-          Pretype_errors.error_actual_type_core env sigma'
-            {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
-            concl;
-        !evdref
+        Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
+                                cl.cl_concl concl sigma'
       in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
-  end }
+
+let unify_resolve_refine poly flags gl clenv =
+  Proofview.tclORELSE
+    (unify_resolve_refine poly flags gl clenv)
+    (fun ie ->
+      match fst ie with
+      | Evarconv.UnableToUnify _ ->
+         Tacticals.New.tclZEROMSG (str "Unable to unify")
+      | e when CErrors.noncritical e ->
+         Tacticals.New.tclZEROMSG (str "Unexpected error")
+      | _ -> iraise ie)
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -291,9 +300,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
 let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter { enter = begin fun gl ->
-     match clenv_of_prods poly nprods (c, clenv) gl with
-     | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
-     | Some (diff, clenv') -> f.enter gl (c, diff, clenv') end }
+      try match clenv_of_prods poly nprods (c, clenv) gl with
+          | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+          | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
+      with e when CErrors.noncritical e ->
+        Tacticals.New.tclZEROMSG (CErrors.print e) end }
   else Proofview.Goal.enter
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
@@ -308,7 +319,7 @@ let matches_pattern concl pat =
        if Constr_matching.is_matching env sigma pat concl then
          Proofview.tclUNIT ()
        else
-         Tacticals.New.tclZEROMSG (str "conclPattern")
+         Tacticals.New.tclZEROMSG (str "pattern does not match")
   in
    Proofview.Goal.enter { enter = fun gl ->
      let env = Proofview.Goal.env gl in
@@ -336,10 +347,19 @@ let pr_gls sigma gls =
 let shelve_dependencies gls =
   let open Proofview in
   tclEVARMAP >>= fun sigma ->
-  (if !typeclasses_debug > 1 then
-     Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls);
+  (if !typeclasses_debug > 1 && List.length gls > 0 then
+     Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
    shelve_goals gls)
 
+let hintmap_of sigma hdc secvars concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none secvars db
+  | Some hdc ->
+     fun db ->
+     if Hint_db.use_dn db then (* Using dnet *)
+       Hint_db.map_eauto sigma secvars hdc concl db
+     else Hint_db.map_existential sigma secvars hdc concl db
+
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
   let open Tacticals.New in
@@ -375,20 +395,20 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
   let nprods = List.length prods in
   let freeze =
     try
-      let cl = Typeclasses.class_info (fst hdc) in
-        if cl.cl_strict then
-          Evarutil.undefined_evars_of_term sigma concl
-        else Evar.Set.empty
+      match hdc with
+      | Some (hd,_) when only_classes ->
+         let cl = Typeclasses.class_info hd in
+         if cl.cl_strict then
+           Evarutil.undefined_evars_of_term sigma concl
+         else Evar.Set.empty
+      | _ -> Evar.Set.empty
     with e when CErrors.noncritical e -> Evar.Set.empty
   in
+  let hint_of_db = hintmap_of sigma hdc secvars concl in
   let hintl =
     List.map_append
       (fun db ->
-        let tacs =
-          if Hint_db.use_dn db then (* Using dnet *)
-            Hint_db.map_eauto sigma secvars hdc concl db
-          else Hint_db.map_existential sigma secvars hdc concl db
-        in
+        let tacs = hint_of_db 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)
@@ -401,8 +421,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
              let tac =
                with_prods nprods poly (term,cl)
                           ({ enter = fun gl clenv ->
-                             (matches_pattern concl p) <*>
-                               ((unify_resolve_refine poly flags).enter gl clenv)})
+                             matches_pattern concl p <*>
+                               unify_resolve_refine poly flags gl clenv})
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -416,8 +436,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
            if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods poly (term,cl)
                   ({ enter = fun gl clenv ->
-                             (matches_pattern concl p) <*>
-                               ((unify_resolve_refine poly flags).enter gl clenv)})) in
+                             matches_pattern concl p <*>
+                             unify_resolve_refine poly flags gl clenv})) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -427,7 +447,15 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
              else
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+        | Give_exact (c,clenv) ->
+           if get_typeclasses_filtered_unification () then
+             let tac =
+               matches_pattern concl p <*>
+                 Proofview.Goal.nf_enter
+                   { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
+             Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
+           else
+             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
@@ -452,16 +480,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
+  let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars
-     (decompose_app_bound sigma concl) true only_classes sigma concl
-  with Bound | Not_found -> []
+    e_my_find_search db_list local_db secvars hd true only_classes sigma concl
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db secvars only_classes sigma concl =
+  let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars
-      (decompose_app_bound sigma concl) false only_classes sigma concl
-  with Bound | Not_found -> []
+    e_my_find_search db_list local_db secvars hd false only_classes sigma concl
+  with Not_found -> []
 
 let cut_of_hints h =
   List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
@@ -470,7 +498,16 @@ let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
+(* alternate separators in debug search path output *)
+let debug_seps = [| "." ; "-" |]
+let next_sep seps = 
+  let num_seps = Array.length seps in
+  let sep_index = ref 0 in
+  fun () ->
+    let sep = seps.(!sep_index) in
+    sep_index := (!sep_index + 1) mod num_seps;
+    str sep
+let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l)
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
@@ -540,10 +577,16 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       let name = PathHints [VarRef id] in
       let hints =
         if is_class then
-          let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+          let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
             (List.map_append
-               (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
-                  (true,false,Flags.is_verbose()) pri false
+             (fun (path,info,c) ->
+	      let info =
+		{ info with Vernacexpr.hint_pattern =
+			    Option.map (Constrintern.intern_constr_pattern env)
+				       info.Vernacexpr.hint_pattern }
+	      in
+	      make_resolves env sigma ~name:(PathHints path)
+                  (true,false,Flags.is_verbose()) info false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
@@ -567,7 +610,7 @@ let make_hints g st only_classes sign =
         in
         if consider then
           let hint =
-            pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+            pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
           in hint @ hints
         else hints)
       ([]) sign
@@ -636,7 +679,7 @@ module V85 = struct
             let env = Goal.V82.env s g' in
             let context = EConstr.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
+              (true,false,false) info.only_classes empty_hint_info (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
@@ -880,19 +923,20 @@ module V85 = struct
   let eauto_tac hints =
     then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
 
-  let eauto_tac depth hints =
-    if get_typeclasses_iterative_deepening () then
-      match depth with
-      | None -> fix_iterative (eauto_tac hints)
-      | Some depth -> fix_iterative_limit depth (eauto_tac hints)
-    else
-      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 eauto_tac strategy depth hints =
+    match strategy with
+    | Bfs -> 
+       begin match depth with
+       | None -> fix_iterative (eauto_tac hints)
+       | Some depth -> fix_iterative_limit depth (eauto_tac hints) end
+    | Dfs ->
+       match depth with
+       | None -> fix (eauto_tac hints)
+       | Some depth -> fix_limit depth (eauto_tac hints)
+                                
+  let real_eauto ?depth strategy unique st hints p evd =
     let res =
-      run_on_evars ~st ~unique p evd hints (eauto_tac depth hints)
+      run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints)
     in
     match res with
     | None -> evd
@@ -905,12 +949,18 @@ module V85 = struct
 
   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 strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in
+    real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd
+
+  let eauto85 ?(only_classes=true) ?st ?strategy depth hints g =
+    let strategy =
+      match strategy with
+      | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs
+      | Some s -> s
+    in
     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
+    match run_tac (eauto_tac strategy depth hints) gl with
     | None -> raise Not_found
     | Some {it = goals; sigma = s; } ->
        {it = List.map fst goals; sigma = s;}
@@ -987,6 +1037,18 @@ module Search = struct
 	Evd.add sigma gl evi')
       sigma goals
 
+  let fail_if_nonclass info =
+    Proofview.Goal.enter { enter = fun gl ->
+      let gl = Proofview.Goal.assume gl in
+      let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+      if is_class_type sigma (Proofview.Goal.concl gl) then
+        Proofview.tclUNIT ()
+      else (if !typeclasses_debug > 1 then
+              Feedback.msg_debug (pr_depth info.search_depth ++
+                                    str": failure due to non-class subgoal " ++
+                                    pr_ev sigma (Proofview.Goal.goal gl));
+            Proofview.tclZERO NotApplicableEx) }
+
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
       depending on the dependencies of the goal and the unique/Prop
@@ -1019,13 +1081,18 @@ module Search = struct
     let foundone = ref false in
     let rec onetac e (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 " ++
+      let pr_error ie =
+        if !typeclasses_debug > 1 then
+          let msg =
+            pr_depth (!idx :: info.search_depth) ++ str": " ++
               Lazy.force pp ++
               (if !foundone != true then
                  str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
-               else mt ())));
+               else mt ())
+          in
+          Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie)
+        else ()
+      in
       let tac_of gls i j = Goal.enter { enter = fun gl' ->
         let sigma' = Goal.sigma gl' in
         let s' = Sigma.to_evar_map sigma' in
@@ -1068,12 +1135,12 @@ module Search = struct
           else tclDISPATCH
                  (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
         in
-        let finish sigma =
+        let finish nestedshelf sigma =
           let filter ev =
             try
               let evi = Evd.find_undefined sigma ev in
               if info.search_only_classes then
-                Some (ev, is_class_evar sigma evi)
+                Some (ev, not (is_class_evar sigma evi))
               else Some (ev, true)
             with Not_found -> None
           in
@@ -1091,9 +1158,9 @@ module Search = struct
           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
+            let shelved, goals = List.partition (fun (ev, s) -> s) remaining in
+            let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in
+            if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then
               Feedback.msg_debug
                 (str"Adding shelved subgoals to the search: " ++
                  prlist_with_sep spc (pr_ev sigma) goals ++
@@ -1106,13 +1173,23 @@ module Search = struct
 	         with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>=
                       fun s -> result s i (Some (Option.default 0 k + j)))
           end
-        in res <*> tclEVARMAP >>= finish
+        in with_shelf res >>= fun (sh, ()) ->
+           tclEVARMAP >>= finish sh
       in
       if path_matches derivs [] then aux e tl
-      else ortac
-             (with_shelf tac >>= fun s ->
+      else
+        let filter =
+          if false (* in 8.6, still allow non-class subgoals
+                    info.search_only_classes *) then fail_if_nonclass info
+          else Proofview.tclUNIT ()
+        in
+        ortac
+             (with_shelf (tac <*> filter) >>= fun s ->
               let i = !idx in incr idx; result s i None)
-             (fun e' -> aux (merge_exceptions e e') tl)
+             (fun e' ->
+	      if CErrors.noncritical (fst e') then
+                (pr_error e'; aux (merge_exceptions e e') tl)
+              else iraise e')
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
@@ -1142,10 +1219,11 @@ module Search = struct
     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
+                       (true,false,false) info.search_only_classes empty_hint_info 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") }
+      { info with search_hints = ldb; last_tac = lazy (str"intro");
+        search_depth = 1 :: 1 :: info.search_depth }
     in kont info'
 
   let intro info kont =
@@ -1173,9 +1251,12 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in
-    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
-    search_tac hints depth 1 info
+    if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
+      Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
+    else
+      let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in
+      let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+      search_tac hints depth 1 info
 
   let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
     let open Proofview in
@@ -1206,16 +1287,24 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints =
+  let eauto_tac ?(st=full_transparent_state) ?(unique=false)
+                ~only_classes ?strategy ~depth ~dep hints =
+    let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
-      if get_typeclasses_iterative_deepening () then
+      let dfs =
+        match strategy with
+        | None -> not (get_typeclasses_iterative_deepening ())
+        | Some Dfs -> true
+        | Some Bfs -> false
+      in
+      if dfs then
+        let depth = match depth with None -> -1 | Some d -> d in
+        search depth
+      else
         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
@@ -1225,10 +1314,28 @@ module Search = struct
          Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
                                     (if Option.is_empty depth then mt()
                                      else str" without reaching its limit"))
+      | Proofview.MoreThanOneSuccess ->
+         Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
+                                  str"more than one success found")
       | e -> Proofview.tclZERO ~info:ie e
-    in Proofview.tclOR tac error
-
-  let run_on_evars ?(unique=false) p evm tac =
+    in
+    let tac = Proofview.tclOR tac error in
+    let tac =
+      if unique then
+        Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
+      else tac
+    in
+    with_shelf numgoals >>= fun (initshelf, i) ->
+    (if !typeclasses_debug > 1 then
+       Feedback.msg_debug (str"Starting resolution with " ++ int i ++
+                             str" goal(s) under focus and " ++
+                             int (List.length initshelf) ++ str " shelved goal(s)" ++
+                             (if only_classes then str " in only_classes mode" else str " in regular mode") ++
+                             match depth with None -> str ", unbounded"
+                                            | Some i -> str ", with depth limit " ++ int i));
+    tac
+
+  let run_on_evars 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') ->
@@ -1260,16 +1367,15 @@ module Search = struct
          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
+  let evars_eauto depth only_classes unique dep st hints p evd =
+    let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+    let res = run_on_evars p evd eauto_tac in
     match res with
     | None -> evd
     | 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
+    evars_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 *)
@@ -1280,11 +1386,9 @@ module Search = struct
 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 =
+                      ?strategy ~depth dbs =
   let dbs = List.map_filter
               (fun db -> try Some (searchtable_map db)
                       with e when CErrors.noncritical e -> None)
@@ -1295,10 +1399,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
   if get_typeclasses_legacy_resolution () then
     Proofview.V82.tactic
     (fun gl ->
-      try V85.eauto85 depth ~only_classes ~st dbs gl
+      try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl
       with Not_found ->
 	Refiner.tclFAIL 0 (str"Proof search failed") gl)
-  else eauto depth ~only_classes ~st ~dep:true dbs
+  else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
@@ -1441,7 +1545,7 @@ let initial_select_evars filter =
 
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
   let evd =
-    try Evarconv.consider_remaining_unif_problems
+    try Evarconv.solve_unif_constraints_with_heuristics
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with e when CErrors.noncritical e -> evd
   in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 8855093ee9..a38be5972f 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -21,7 +21,11 @@ val get_typeclasses_debug : unit -> bool
 val set_typeclasses_depth : int option -> unit
 val get_typeclasses_depth : unit -> int option
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
+type search_strategy = Dfs | Bfs
+
+val set_typeclasses_strategy : search_strategy -> unit
+
+val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy ->
                         depth:(Int.t option) ->
                         Hints.hint_db_name list -> unit Proofview.tactic
 
@@ -37,8 +41,12 @@ module Search : sig
   val eauto_tac :
     ?st:Names.transparent_state ->
     (** The transparent_state used when working with local hypotheses  *)
+    ?unique:bool ->
+    (** Should we force a unique solution *)
     only_classes:bool ->
     (** Should non-class goals be shelved and resolved at the end *)
+    ?strategy:search_strategy ->
+    (** Is a traversing-strategy specified? *)
     depth:Int.t option ->
     (** Bounded or unbounded search *)
     dep:bool ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 14082bb8dc..e0dff3739d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -417,9 +417,7 @@ let eauto ?(debug=Off) np lems dbnames =
   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
+  let db_list = current_pure_db () in
   tclTRY (e_search_auto debug n lems db_list) gl
 
 let gen_eauto ?(debug=Off) np lems = function
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6fcf529c28..53b468bff7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
 open Pp
 open CErrors
 open Util
@@ -731,7 +732,7 @@ let find_positions env sigma t1 t2 =
     let hd1,args1 = whd_all_stack env sigma t1 in
     let hd2,args2 = whd_all_stack env sigma t2 in
     match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with
-      | Construct (sp1,_), Construct (sp2,_)
+      | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
 	  let sorts' =
@@ -740,11 +741,15 @@ let find_positions env sigma t1 t2 =
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if eq_constructor sp1 sp2 then
-	    let nrealargs = constructor_nrealargs_env env sp1 in
-	    let rargs1 = List.lastn nrealargs args1 in
-	    let rargs2 = List.lastn nrealargs args2 in
+	    let nparams = inductive_nparams_env env ind1 in
+	    let params1,rargs1 = List.chop nparams args1 in
+	    let _,rargs2 = List.chop nparams args2 in
+            let (mib,mip) = lookup_mind_specif env ind1 in
+            let params1 = List.map EConstr.Unsafe.to_constr params1 in
+            let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
+            let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
-	      (List.map2_i (fun i -> findrec sorts' ((sp1,i)::posn))
+	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
 	  else if Sorts.List.mem InType sorts'
           then (* see build_discriminator *)
@@ -1180,7 +1185,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
-	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
+	let () =
+          evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a1c99c341e..77ed4330c1 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -94,6 +94,10 @@ let secvars_of_hyps hyps =
   if all then Id.Pred.full (* If the whole section context is available *)
   else pred
 
+let empty_hint_info =
+  let open Vernacexpr in
+  { hint_priority = None; hint_pattern = None }
+
 (************************************************************************)
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
@@ -106,18 +110,25 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument (* Hint Extern *)
 
-type hints_path_atom = 
-  | PathHints of global_reference list
+
+type 'a hints_path_atom_gen =
+  | PathHints of 'a list
+  (* For forward hints, their names is the list of projections *)
   | PathAny
 
-type hints_path =
-  | PathAtom of hints_path_atom
-  | PathStar of hints_path
-  | PathSeq of hints_path * hints_path
-  | PathOr of hints_path * hints_path
+type hints_path_atom = global_reference hints_path_atom_gen
+
+type 'a hints_path_gen =
+  | PathAtom of 'a hints_path_atom_gen
+  | PathStar of 'a hints_path_gen
+  | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+  | PathOr of 'a hints_path_gen * 'a hints_path_gen
   | PathEmpty
   | PathEpsilon
 
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+
 type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
@@ -399,21 +410,40 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
-let pp_hints_path_atom a =
+let pp_hints_path_atom prg a =
   match a with
   | PathAny -> str"_"
-  | PathHints grs -> pr_sequence pr_global grs
-					   
-let rec pp_hints_path = function
-  | PathAtom pa -> pp_hints_path_atom pa
-  | PathStar (PathAtom PathAny) -> str"_*"
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
-  | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p'
-  | PathOr (p, p') -> 
-     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++
-       pp_hints_path p' ++ str ")"
+  | PathHints grs -> pr_sequence prg grs
+
+let pp_hints_path_gen prg =
+  let rec aux = function
+    | PathAtom pa -> pp_hints_path_atom prg pa
+    | PathStar (PathAtom PathAny) -> str"_*"
+    | PathStar p -> str "(" ++ aux p ++ str")*"
+    | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
+    | PathOr (p, p') -> 
+     str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++
+     aux p' ++ str ")"
   | PathEmpty -> str"emp"
   | PathEpsilon -> str"eps"
+  in aux
+     
+let pp_hints_path = pp_hints_path_gen pr_global
+
+let glob_hints_path_atom p =
+  match p with
+  | PathHints g -> PathHints (List.map Nametab.global g)
+  | PathAny -> PathAny
+
+let glob_hints_path =
+  let rec aux = function
+    | PathAtom pa -> PathAtom (glob_hints_path_atom pa)
+    | PathStar p -> PathStar (aux p)
+    | PathSeq (p, p') -> PathSeq (aux p, aux p')
+    | PathOr (p, p') -> PathOr (aux p, aux p')
+    | PathEmpty -> PathEmpty
+    | PathEpsilon -> PathEpsilon
+  in aux
 
 let subst_path_atom subst p =
   match p with
@@ -704,8 +734,7 @@ let searchtable_add (name,db) =
 let current_db_names () = Hintdbmap.domain !searchtable
 let current_db () = Hintdbmap.bindings !searchtable
 
-let current_pure_db () =
-  List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
+let current_pure_db () = List.map snd (current_db ())
 
 let error_no_such_hint_database x =
   user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".")
@@ -757,7 +786,7 @@ let secvars_of_constr env sigma c =
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
 
-let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
     match EConstr.kind sigma cty with
@@ -768,16 +797,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
 	in
-          (Some hd,
-	  { pri = (match pri with None -> 0 | Some p -> p);
-	    poly = poly;
-	    pat = Some pat;
-	    name = name;
-            db = None;
-            secvars;
-	    code = with_uid (Give_exact (c, cty, ctx)); })
+	let pri = match info.hint_priority with None -> 0 | Some p -> p in
+	let pat = match info.hint_pattern with
+	| Some pat -> snd pat
+	| None -> pat
+	in
+        (Some hd,
+	 { pri; poly; pat = Some pat; name;
+	   db = None; secvars;
+	   code = with_uid (Give_exact (c, cty, ctx)); })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match EConstr.kind sigma cty with
     | Prod _ ->
@@ -790,12 +820,13 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
           with BoundPattern -> failwith "make_apply_entry" in
         let nmiss = List.length (clenv_missing ce) in
         let secvars = secvars_of_constr env sigma c in
+	let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
+	let pat = match info.hint_pattern with
+	| Some p -> snd p | None -> pat
+	in
 	if Int.equal nmiss 0 then
 	  (Some hd,
-          { pri = (match pri with None -> nb_hyp sigma' cty | Some p -> p);
-	    poly = poly;
-            pat = Some pat;
-	    name = name;
+          { pri; poly; pat = Some pat; name;
             db = None;
             secvars;
             code = with_uid (Res_pf(c,cty,ctx)); })
@@ -805,12 +836,8 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++
 	    str " will only be used by eauto");
           (Some hd,
-           { pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
-	     poly = poly;
-             pat = Some pat;
-	     name = name;
-             db = None;
-             secvars;
+           { pri; poly; pat = Some pat; name;
+	     db = None; secvars;
              code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
@@ -862,14 +889,14 @@ let fresh_global_or_constr env sigma poly cr =
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags pri poly ?name cr =
+let make_resolves env sigma flags info poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-                             [make_exact_entry env sigma pri poly ?name;
-                              make_apply_entry env sigma flags pri poly ?name]
+			     [make_exact_entry env sigma info poly ?name;
+			      make_apply_entry env sigma flags info poly ?name]
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
@@ -883,7 +910,7 @@ let make_resolve_hyp env sigma decl =
   let hname = NamedDecl.get_id decl in
   let c = mkVar hname in
   try
-    [make_apply_entry env sigma (true, true, false) None false
+    [make_apply_entry env sigma (true, true, false) empty_hint_info false
        ~name:(PathHints [VarRef hname])
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
@@ -1169,16 +1196,17 @@ let add_transparency l b local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_extern pri pat tacast local dbname =
-  let pat = match pat with
+let add_extern info tacast local dbname =
+  let pat = match info.hint_pattern with
   | None -> None
   | Some (_, pat) -> Some pat
   in
-  let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
+  let hint = make_hint ~local dbname
+		       (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
-let add_externs pri pat tacast local dbnames =
-  List.iter (add_extern pri pat tacast local) dbnames
+let add_externs info tacast local dbnames =
+  List.iter (add_extern info tacast local) dbnames
 
 let add_trivials env sigma l local dbnames =
   List.iter
@@ -1190,15 +1218,16 @@ let add_trivials env sigma l local dbnames =
 
 type hnf = bool
 
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
 type hints_entry =
-  | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
+  | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
-  | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
+  | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1265,11 +1294,12 @@ let interp_hints poly =
 	(PathHints [gr], poly, IsGlobRef gr)
     | HintsConstr c -> (PathAny, poly, f poly c)
   in
-  let fres (pri, b, r) =
+  let fp = Constrintern.intern_constr_pattern (Global.env()) in
+  let fres (info, b, r) =
     let path, poly, gr = fi r in
-      (pri, poly, b, path, gr)
+    let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
+      (info, poly, b, path, gr)
   in
-  let fp = Constrintern.intern_constr_pattern (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
@@ -1285,7 +1315,7 @@ let interp_hints poly =
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
-			None, mib.Declarations.mind_polymorphic, true, 
+			empty_hint_info, mib.Declarations.mind_polymorphic, true,
 			PathHints [gr], IsGlobRef gr)
       in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
@@ -1294,7 +1324,7 @@ let interp_hints poly =
       let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
       let env = Genintern.({ genv = env; ltacvars }) in
       let _, tacexp = Genintern.generic_intern env tacexp in
-      HintsExternEntry (pri, pat, tacexp)
+      HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
 let add_hints local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
@@ -1310,8 +1340,8 @@ let add_hints local dbnames0 h =
   | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local dbnames
-  | HintsExternEntry (pri, pat, tacexp) ->
-      add_externs pri pat tacexp local dbnames
+  | HintsExternEntry (info, tacexp) ->
+      add_externs info tacexp local dbnames
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
@@ -1335,7 +1365,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
     List.map_append (fun (poly, lem) ->
-		     make_resolves env sigma (eapply,true,false) None poly lem) lems in
+		     make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
@@ -1389,7 +1419,9 @@ let pr_hint h = match h.obj with
       (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
-  (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+  let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
+  (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+   ++ str", id " ++ int id ++ str ")" ++ spc ())
 
 let pr_hint_list hintlist =
   (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 0d6dd434e9..467fd46d53 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -31,6 +31,8 @@ type debug = Debug | Info | Off
 
 val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
 
+val empty_hint_info : 'a hint_info_gen
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -44,11 +46,12 @@ type 'a hint_ast =
 type hint
 type raw_hint = constr * types * Univ.universe_context_set
 
-type hints_path_atom = 
-  | PathHints of global_reference list
+type 'a hints_path_atom_gen =
+  | PathHints of 'a list
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
+type hints_path_atom = global_reference hints_path_atom_gen
 type hint_db_name = string
 
 type 'a with_metadata = private {
@@ -69,20 +72,28 @@ type search_entry
 
 type hint_entry
 
-type hints_path =
-  | PathAtom of hints_path_atom
-  | PathStar of hints_path
-  | PathSeq of hints_path * hints_path
-  | PathOr of hints_path * hints_path
+type 'a hints_path_gen =
+  | PathAtom of 'a hints_path_atom_gen
+  | PathStar of 'a hints_path_gen
+  | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+  | PathOr of 'a hints_path_gen * 'a hints_path_gen
   | PathEmpty
   | PathEpsilon
 
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+    
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
-val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
+val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds
+val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 val pp_hint_mode : hint_mode -> Pp.std_ppcmds
+val glob_hints_path_atom :
+  Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+val glob_hints_path :
+  Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
 
 module Hint_db :
   sig
@@ -133,20 +144,21 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
 type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
 type hints_entry =
-  | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * 
-			  hint_term) list
+  | HintsResolveEntry of
+    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
-  | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
+  | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -173,23 +185,34 @@ val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
   env -> evar_map -> evar_map * constr -> hint_term
 
-(** [make_exact_entry pri (c, ctyp, ctx, secvars)].
+(** [make_exact_entry info (c, ctyp, ctx)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c].
-   [ctx] is its (refreshable) universe context. *)
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> 
+   [ctx] is its (refreshable) universe context. 
+   In info:
+   [hint_priority] is the hint's desired priority, it is 0 if unspecified
+   [hint_pattern] is the hint's desired pattern, it is inferred if not specified
+*)
+
+val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)].
+(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
    [eapply] is true if this hint will be used only with EApply;
    [hnf] should be true if we should expand the head of cty before searching for
    products;
    [c] is the term given as an exact proof to solve the goal;
    [cty] is the type of [c].
-   [ctx] is its (refreshable) universe context. *)
+   [ctx] is its (refreshable) universe context. 
+   In info:
+   [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
+   if unspecified
+   [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty]
+   if not specified
+*)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -200,7 +223,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 27c1987a06..a1cd510475 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -337,6 +337,16 @@ module New = struct
           catch_failerror e <*> t2
         end
     end
+
+  let tclORELSE0L t1 t2 =
+    tclINDEPENDENTL begin
+      tclORELSE
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2
+        end
+    end
+
   let tclORELSE t1 t2 =
     tclORELSE0 (tclPROGRESS t1) t2
 
@@ -388,6 +398,9 @@ module New = struct
 
   let tclTRY t =
     tclORELSE0 t (tclUNIT ())
+  
+  let tclTRYb t =
+    tclORELSE0L (t <*> tclUNIT true) (tclUNIT false)
 
   let tclIFTHENELSE t1 t2 t3 =
     tclINDEPENDENT begin
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index c9ff777164..5839666a73 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -207,6 +207,7 @@ module New : sig
   val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic
 
   val tclTRY : unit tactic -> unit tactic
+  val tclTRYb : unit tactic -> bool list tactic
   val tclFIRST : unit tactic list -> unit tactic
   val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
   val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5ad43a7d60..f8cbc2671f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -90,7 +90,7 @@ let _ =
 
 let apply_solve_class_goals = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optsync = true; Goptions.optdepr = true;
   Goptions.optname =
     "Perform typeclass resolution on apply-generated subgoals.";
   Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
@@ -1150,7 +1150,7 @@ let run_delayed env sigma c =
 
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
+  Pretyping.solve_unification_constraints = true;
   Pretyping.use_hook = Some solve_by_implicit_tactic;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
@@ -2740,7 +2740,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter { enter = begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let t = Tacmach.New.pf_get_type_of gl c in
       let sigma = Tacmach.New.project gl in
       let hd = head_ident sigma c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
@@ -5035,9 +5035,16 @@ module New = struct
   open Locus
 
   let reduce_after_refine =
+    let onhyps =
+      (** We reduced everywhere in the hyps before 8.6 *)
+      if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
+      then None
+      else Some []
+    in
     reduce
-      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences }
+      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
+	     rZeta=false;rDelta=false;rConst=[]})
+      {onhyps; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Refine.refine ?unsafe c <*>