The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Adam Chlipala 
>>>>> <adamc AT csail.mit.edu>
>>>>>  writes:

> Most likely the term you're giving to replace doesn't match the one found in
> the subgoal, considering implicit arguments, notations, etc.  Try running
> [Set Printing All], and using a tactic like [pose] to bring the arguments to
> [replace] into the subgoal, so you can compare them against what appeared
> originally.

Yes, I run into this exact issue quite regularly, where sometimes a value was
destructed too late, so that some values in scope have the original form, and
others have the destructed form, but you can only see this difference using
Set Printing All.  For example: where "fmap" is one case uses a Functor
instance in scope, while another "fmap" is using an "is_functor" coercion from
the Monad in scope.

John