Ssreflect Users Discussion List

[Maxime Dénès <>]

Yes, it works perfectly, even on the real proof.

Thank you !
Maxime.

On 28/12/2011 13:13, Cyril Cohen wrote:
> Hello, it's committed. I tried your example on my computer and got :
>
> Goal ('X - A%:P) * ('X - A%:P) = ('X - A%:P) * ('X - A%:P).
> Time set x := ('X - B%:P) * ('X - B%:P).
> Finished transaction in 0. secs (0.073328u,0.003333s)
>
> I hope it will be the same for you. Bye.