The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello

> On a related note, regarding this particular development, there are a
> lot of proofs that were discharged by 'Auto' but now I find myself
> needing to use 'firstorder'. It is safe to conclude that that
> Auto/auto became less powerful through the years?

You might want to look at section 8.13.2 of the manual. There you find:

There is also a special database called v62. It collects all hints that
were declared in the versions of Coq prior to version 6.2.4 when the
databases core, arith, and so on were introduced. The purpose of the
database v62 is to ensure compatibility with further versions of Coq for
developments done in versions prior to 6.2.4 (auto being replaced by
auto with v62). The database v62 is intended not to be extended (!). It
is not included in the hint databases list used in the auto with *
tactic.

Hope that clarifies things

Regards
Christian