From 177d593b33af16fb484f7f0e2da772b95b3cdc6c Mon Sep 17 00:00:00 2001
From: thery
Date: Tue, 19 Jun 2007 16:58:13 +0000
Subject: safe_shift recursion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9897 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Ints/num/NMake.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index be35b5fea1..5a441d8b47 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -3858,7 +3858,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple
   Definition safe_shiftl n x :=
     itert _ double_size (shiftl n) 
       (fun x => match compare n (head0 x) with Gt => false | _ => true end) 
-       (digits x) x.
+       (digits n) x.
  
  Definition is_even x :=
   match x with
-- 
cgit v1.2.3