From 7b64e1d3b368bca3c8b4ebe2ccacdf6d79eef815 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 May 2011 15:12:40 +0000
Subject: Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zpower.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/ZArith')

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index c021b01a96..ce99427f2d 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -243,7 +243,7 @@ Section power_div_with_rest.
 	simpl in |- *;
 	  [ trivial with zarith
 	    | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *;
-	      elim (iter_nat n (Z * Z * Z) Zdiv_rest_aux (x, 0, 1));
+	      elim (iter_nat n _ Zdiv_rest_aux (x, 0, 1));
 		destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z);
 		  assumption ].
   Qed.
@@ -302,7 +302,7 @@ Section power_div_with_rest.
   Proof.
     intros x p.
     generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-    elim (iter_pos p (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)).
+    elim (iter_pos p _ Zdiv_rest_aux (x, 0, 1)).
     simple induction a.
     intros.
     elim H; intros H1 H2; clear H.
-- 
cgit v1.2.3