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 +++++++++++ theories/Init/Peano.v | 4 +++- 2 files changed, 14 insertions(+), 1 deletion(-) 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. -- cgit v1.2.3