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: "John Wiegley" <johnw AT newartisans.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Replace does not work
  • Date: Tue, 07 Oct 2014 15:48:11 -0500
  • Organization: New Artisans LLC

>>>>> 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



Archive powered by MHonArc 2.6.18.

Top of Page