NArith: Definition of a Npow power function

 By the way, adds an Piter_op iterator :
 Piter_op op p a is "a op a ... op a" with a occurring p times.
 It could be use to define Pmult_nat and hence nat_of_P (not
 fully done for maintaining compatibility).
 Unlike iter_pos, Piter_op is logarithmic in p, not linear.

 Note: We should adapt someday the brain-damaged Zpower to make it
 use Piter_op instead of iter_pos.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions