The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

> 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?
>

Hm, I would suspect that instead you have not configured your hint
databases correctly, first...

kris