diff options
| -rw-r--r-- | test-suite/success/Hints.v | 11 | ||||
| -rw-r--r-- | theories/Init/Peano.v | 4 |
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 73c8c5ef4..d5322d094 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -92,7 +92,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. |