The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

> Well, it IS more readable, no doubt about it. I see 2 possible answers that 
> would solve my problem:
> * having a flag to turn it down if wanted
> * using a different pow such that a^2=a*a, knowing that this pow will be 
> used in a^b with b >=2 (this is the real case as ring_simplify will use pow 
> only when it is at least a square.

I would vote for 2 but I' m scare it would break many proofs in the
real library.
A third solution is to rewrite with the ad-hoc theorem x^2 = x * x when 
needed.

--
Laurent