From 8db43cac35eaa8f2b8c4f8d777dfaafd1f02f27e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 16:11:47 +0200
Subject: Do not do a round trip with auto hint representation in autoapply.

---
 tactics/class_tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 5a8522359d..6c1bdca682 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1231,8 +1231,7 @@ let autoapply c i =
     (Hints.Hint_db.transparent_state hintdb) in
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
-    unify_resolve ~with_evars:true flags h None <*>
+  Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
-- 
cgit v1.2.3