The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/03/2012 10:44 AM, Eric Finster wrote:
> 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?
>    

My first guess is that implicit arguments are being resolved differently 
in the goal vs. the first argument you pass to [change].  Perhaps [Set 
Printing All] would help see the difference.