The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

2011/11/30 Damien Pous 
<Damien.Pous AT inria.fr>:

> I only partly agree on this point:
> - yes, such an interface tool would be great,
> - but there are situations where you want to keep [(e)auto] in the
> source because it's possibly more robust to small changes in the
> definitions.
> (e.g., when you change the order of the hypotheses of some hint, when
> you remove hypotheses of some hint, or when you change the hypotheses
> of the current goal).
>
> So maybe the interface you want to implement should be able to recall
> that some sequence of lemma applications was found with [(e)auto], so
> that this sequence can easily be recomputed when it breaks.

This is exactly what I have in mind:

replace eauto by:

solve [ <what eauto did> | idtac "Something went wrong here, trying
eauto instead" ; eauto | idtac "even eauto went wrong" ]

And have the interface replacing <what eauto did> by the new tactic
found when necessary.

P.