The Coq mailing list

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

Le Thu, 04 Oct 2012 00:16:37 +0200,
Jonas Oberhauser 
<s9joober AT gmail.com>
 a écrit :

> Hi all,
> 
> 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?
> 
> Kind regards, Jonas

I forgot to add in my reply that the type of 'x' here is 'nat', and
'nat' has no occurrence of '3+2', that is why there is a reported
failure. Anyway it definetely is not a bug.