From 993e6a0df37216908ea566361d1f5e527e82b1e1 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Fri, 29 Dec 2017 16:21:14 +0100
Subject: Fix core hint database issue #6521

---
 test-suite/success/Hints.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 6962e43e7e..8d08f5975e 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.
-- 
cgit v1.2.3