The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 4 Oct 2012 02:26:50 +0200,
Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 a écrit :

> Hi,
> 
> > This example describes a "problem" I have encountered recently:
> > 
> > Goal True.
> > pose (x := 3+2).
> > assert (3+2 = 5) by auto.
> > rewrite H in x.
> > (* Error: Found no subterm matching "3 + 2" in x. *)
> > 
> > Is this a bug?
> 
> In some sense yes. The general pattern for a local definition H in the
> goal context is that "in H" applies to both value and type of the
> definition, while "in (value of x)" and "in (type of x)" select the
> value or type respectively. For instance, both of
> 
>   change (3+2) with 5 in x.
>   change (3+2) with 5 in (value of x).
> 
> would work here. However, "rewrite ... in ..." does not care about the
> value and hence does not follow this pattern. You can fill a request
> for enhancement. In the meantime, you can first "revert" x, "rewrite"
> and re-"intro" x.
>
> Hugo

Hushh, I am not sure to understand what you mean by "revert" x,
"rewrite" and re-"intro" x.

For me "revert x", would generalize over