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

Reviewed-by: mattam82

2 files changed, 57 insertions, 3 deletions

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 =
diff --git a/test-suite/bugs/closed/bug_12532.v b/test-suite/bugs/closed/bug_12532.v
new file mode 100644
index 0000000000..665f6643e6
--- /dev/null
+++ b/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.