aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Ints/num/NMake.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index be35b5fea..5a441d8b4 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