The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 10/05/2013 18:02, 
bhandalc AT tcd.ie
 wrote:
> It seems as though eapply doesn't like when you instantiate existentials in 
> a
> hypothesis after the application- they must have existsed beforehand. The
> workaround is simple: Just instantiate before eapply. But I believe the
> behaviour is of interest nonetheless.

If I remember correctly, this bug had already been witnessed (had the
problem with eauto and ring), and it was fixed in 8.4

PMP

Attachment: signature.asc
Description: OpenPGP digital signature