The Coq mailing list

[Eric Finster <ericfinster AT gmail.com>]

Hi All,

I'm trying to replace an expression with another which I know it is
convertible to using the change tactic.  The tactic succeeds without
an error message, but the goal is not updated to the new expression.
As it turns out, I am using roughly the same "change" at another place
in my code but with a simpler expression, and it works fine.  Can
anyone give me a pointer as to why this might happen?

Cheers,

Eric