The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

The tactic psatzl is working fine, thank you for that hint.

I'm still having some other problems, which seem (with regard to the content)
simple. I think it's a problem about type conversion:
I'd like to calculate (or actually replace) (IZR 32 * powerRZ 2 (-5) * x) with
simply x. However, I don't succeed in converting the two parts in such a way
that i can reduce them to get "x" alone.

What am I doing wrong?


Sincerely,