The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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. I need to investigate a bit more to understand
where this comes from.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature