Merge PR #12532: Use the unification result for eauto's eapply.

Reviewed-by: mattam82

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 =

test-suite/bugs/closed/bug_12532.v

@@ -0,0 +1,56 @@
+(** This is a change of behaviour introduced by PR #12532. It is not clear
+    whether it is a legit behaviour but it is worth having it in the test
+    suite. *)
+
+Module Foo.
+
+Axiom whatever : Type.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo : forall st st', In st -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name), In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+solve [debug eauto].
+Abort.
+
+End Foo.
+
+Module Bar.
+
+Axiom whatever : Type.
+Axiom AppendEntries : whatever -> Prop.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo :
+  forall st st' lid,
+    (AppendEntries lid -> In st) -> AppendEntries lid -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name) (w : whatever),
+    AppendEntries w -> In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+intros.
+solve [debug eauto].
+Abort.
+
+End Bar.