diff options
| author |  Anton Trunov <anton.trunov@imdea.org> | 2017-12-29 16:21:14 +0100 |
|---|---|---|
| committer | Anton Trunov <anton.trunov@imdea.org> | 2018-01-03 12:08:41 +0100 |
| commit | 993e6a0df37216908ea566361d1f5e527e82b1e1 (patch) | |
| tree | 126df256db59d9f3e2b606cf8de8be64a98f7792 /test-suite/success | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
Fix core hint database issue #6521
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Hints.v | 11 |
1 files changed, 11 insertions, 0 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. |