Fix core hint database issue #6521

2 files changed, 14 insertions, 1 deletions

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 6962e43e7..8d08f5975 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -172,3 +172,14 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
   Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
 End HintCut.
+
+
+(* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *)
+(* e.g. those tactics when considering a goal with existential varibles *)
+(* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *)
+(* See this Coq club post for more detail: *)
+(* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *)
+
+Goal forall (m : nat), exists n, m = n /\ m = n.
+  intros m; eexists; split; [trivial | reflexivity].
+Qed.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 571d2f2dd..1316b8624 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -90,7 +90,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
   induction n; simpl; auto.
 Qed.
-Hint Resolve plus_n_O: core.
+
+Remove Hints eq_refl : core.
+Hint Resolve plus_n_O eq_refl: core.  (* We want eq_refl to have higher priority than plus_n_O *)
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
 Proof.