The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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