The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

I'm restoring a development from 1998 to work with Coq 8.4 and I'm stuck with some redefined/renamed lemma.

In short, where is the lemma congr_eqT that used to work with Coq v5.8?

  Lemma congr_eqT : (x==y)->((f x)==(f y)) 

 

I tried with SearchPattern, but no luck ...

Help please :-)

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?

Cheers!

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