Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Replace does not work

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Replace does not work


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Replace does not work
  • Date: Tue, 07 Oct 2014 15:42:54 -0400

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.



Archive powered by MHonArc 2.6.18.

Top of Page