The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 06/05/2015 08:00, Vadim Zaliva wrote:

> It now asks me to prove an obligation:
>
> S pad = S p
>
> Which does not make sense!

> This is an artificial example which shows simplified case of a problem I am 
> facing as a part of a more complex proof. I am looking for any explanations 
> on why this is happening and how this could be avoided. Thanks!

This seems to be a bug in Coq, and it seems to have been fixed in 8.5. 
Unfortunately, I have no idea how to work around it in 8.4.

Best regards,

Guillaume