The Coq mailing list

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

On 14/10/2014 17:42, Jonathan wrote:
> Is this a bug, a feature, or not fully developed?

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.

Thus the following hints should be observationally equivalent:

Hint Extern 5 (foo _) => econstructor.
Hint Extern 5 (foo _) => once econstructor.

We should integrate the backtracking behaviour in eauto, but I do not
think it is as easy at it sounds (apart from rewriting it from scratch).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature