The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Dear Adam and John,

Thanks for the replies, I´ve managed to fix the problem.

Best Regards,

Marcus.

2014-10-07 16:42 GMT-03:00 Adam Chlipala <adamc AT csail.mit.edu>:

On 10/07/2014 03:37 PM, Marcus Ramos wrote:

I can´t see why "replace" does not work in the following case. The context is:

[...]

That is, instead of getting a new H1 (with the replacement required) and a corresponding new subogal, I get the same H1 as before and the new subgoal. "simpl in H1" before "replace" does not work as well. Any suggestions?

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.

My guess is there is an issue with [sf] being an alias for [list _].  The goal contains [sf] where your [replace] invocation contains [list _], or the other way around.