The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

2012/9/13 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...

I did...I do not think this is the cause..

 

kris

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.