The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 18/07/2013 06:45, t x a écrit :
> Hi,
>
> Here is my minimal failure case:
>
> https://gist.github.com/anonymous/8ae8b98d037077c9fda1
>
>    Question1: Why can't I do a "rewrite" in a ":=" definition?

I suppose that Coq is trying to rewrite in the type of "b" (as it would 
with a ":" hypothesis) and there are no occurrences of "a" in "nat". I 
have no idea whether rewriting in the type of a let binding is a useful 
behavior.

>    Question2: How can I do what I intend, i.e. do a rewrite in a ":="

You can do it the way people were doing it when "rewrite in" did not yet 
exist:

revert b. rewrite H. intros b.

Best regards,

Guillaume