From d041793ec3cad022ae54e4072f4f4b52b3cd1970 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Jun 2016 18:59:33 +0200
Subject: Fix resolve_one_typeclass to use the new engine

---
 tactics/class_tactics.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a4c068fa63..714e12e3d7 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1458,8 +1458,10 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   let depth = get_typeclasses_depth () in
   let gls' =
     if get_typeclasses_compat () = Flags.Current then
-      Proofview.V82.of_tactic
-        (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:false) gls
+      try
+        Proofview.V82.of_tactic
+        (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
+      with Refiner.FailError _ -> raise Not_found
     else V85.eauto85 depth ~st [hints] gls
   in
   let evd = sig_sig gls' in
-- 
cgit v1.2.3