The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi,

What is the difference between

apply lemma.

and

apply @lemma.

?  I have encountered a few situations where the former fails but the
latter succeeds.  This confuses me, because in both cases all the
arguments of lemma (implicit or non-implicit) have to be deduced from
context.  Is the first one somehow trying to guess the implicit
arguments too soon or without enough information?

Thanks!
Mike