From 189f4182d6e65ada8fb5856b195b52d15bebdf3a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 16 Jun 2020 14:40:41 +0200
Subject: Use the unification result for eauto's eapply.

Instead of dropping the unification result and calling simple eapply with
the original term, we simply use the same code path as auto and typeclass
eauto, i.e. reuse the clenv for refinement.
---
 tactics/eauto.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 0ff90bc046..90e4aaa167 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -69,9 +69,7 @@ let unify_e_resolve flags h =
   Proofview.Goal.enter begin fun gl ->
       let clenv', c = connect_hint_clenv h gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
-      Proofview.tclTHEN
-        (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-        (Tactics.Simple.eapply c)
+      Clenvtac.clenv_refine ~with_evars:true ~with_classes:true clenv'
     end
 
 let hintmap_of sigma secvars concl =
-- 
cgit v1.2.3