The Coq mailing list

[Sylvie.Boldo AT inria.fr]

Hello,

Many thanks Benjamin for the solution modifying ring !!
It works great (and does not get out of sections). I never thought I would 
ever modify ring...


> > 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.
I would vote for 2 too.
I do not think it would break many proofs in the real library. That is 
a new feature and multiplying a number by itself is not such common 
use imho (or people would have complained earlier of the incompatibility)


> A third solution is to rewrite with the ad-hoc theorem x^2 = x * x when 
> needed.
Well, yes... Could work too. But I would prefer an "unfold pow" to a 
"deep look on the goal" and then "rewrite pow_3; repeat rewrite pow_2".

Sylvie