The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/14/2014 12:53 PM, Pierre-Marie Pédrot wrote:
> On 14/10/2014 18:32, Pierre-Marie Pédrot wrote:
> > As far as I know, eauto and auto does not take advantage of the
> > backtracking mechanism of the new tactic monad. It only takes the first
> > result of the tactic.
> Nevermind, it is not the case anymore. The bug seems to come from the
> matching of the conclusion as [foo _] which prevents the hint to apply.
> If you change your first hint to
>
> Hint Extern 5 => econstructor.
>
> Then it magically works.

That doesn't magically work for me.  To be clear, I'm trying:

Inductive foo : nat -> Prop :=
| Foo1 : foo 1
| Foo2 : foo 2.

Hint Extern 5 => econstructor.

Inductive bar : Type :=
| Bar{n}(f : foo n)(neq2 : n = 2) : bar.

Hint Constructors bar.

Goal bar.
Fail solve [eauto].
Fail typeclasses eauto with core.
Abort.

-- Jonathan