The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

M. Scott Doerrie wrote:
> Why won't "rewrite Hopt2 in Hopt6" work.  It fails with: Found no 
> subterm matching "Sem.S.RefMapS.find a s" in Hopt6.  It's clearly 
> present, even when using "Set Printing All."

Assuming that you've eyeballed the code properly and checked that the 
terms really match (which I haven't done), the problem could be that 
[Hopt6] would no longer be well-typed after the rewrite.  I suggest 
running [Check P], where [P] is a hand-rewritten version of the term.  
If this fails, then you'll have the culprit.  The [rewrite] error 
message for cases like this could definitely be improved. ;)