coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. |
- [Coq-Club] Replace does not work, Marcus Ramos, 10/07/2014
- Re: [Coq-Club] Replace does not work, Adam Chlipala, 10/07/2014
- Re: [Coq-Club] Replace does not work, John Wiegley, 10/07/2014
- Re: [Coq-Club] Replace does not work, Marcus Ramos, 10/08/2014
- Re: [Coq-Club] Replace does not work, Adam Chlipala, 10/07/2014
Archive powered by MHonArc 2.6.18.