The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

2011/11/30 Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>:
> Or by going back and replacing eauto by an explicite apply. Actually
> my opinion is that (e)auto (and other automatic tactics) should always
> be used as proof search commands quickly replaced by the succeeding
> tactics they found (side effect: faster scripts, no dependence on hint
> databases). And yes interfaces should help with this, this is on my
> todo list for proofgeneral.

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.

Damien