diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:34:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:34:46 +0100 |
| commit | 866bad4e9cdaa6ff4419840f8c9980f770873176 (patch) | |
| tree | 14fbdbbebd25a4739ded1dcb8570f343c4633333 /test-suite/success | |
| parent | 97498d79324b4890977f0a9077ea4a01bc9cacfe (diff) | |
| parent | 993e6a0df37216908ea566361d1f5e527e82b1e1 (diff) | |
Merge PR #6522: 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. |