The Coq mailing list

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

Le Wed, 23 Jan 2013 23:51:29 +0800,
liheng 
<lihengszh AT gmail.com>
 a écrit :

> Hello.
> The error occurs when runs *x * x + y * x + (x + y) * y = x * x + 2 *
> x 
> * y + y * y *on*rewrite_mult_plus_distr_r?
> *I don't know the problem and the reasons.*
> *thanks*?
> 
> **code is:*
> Require Import Arith.
> Lemma time2 : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.
> Proof.
>   intros x y.
>   SearchRewrite (_ * (_ + _)).
>   rewrite mult_plus_distr_l.
>   SearchRewrite ((_ + _) * _).
>   rewrite mult_plus_distr_r with (p:=x).
>   rewrite_mult_plus_distr_r.
> ...
> *Error: *
> The reference rewrite_mult_plus_distr_r was not found in the current 
> environment.

Just remove your underscore…
rewrite mult_plus_distr_r

instead of

rewrite_mult_plus_distr_r