From 9e37305cc4b817869de98b5cce49d3599d2c0aba Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 4 Feb 2022 20:19:17 +0100
Subject: progress

---
 kvx/FPDivision64.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index ddd96f8e..fc8e6173 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1071,8 +1071,7 @@ Proof.
   intros ; split ; apply le_IZR ; lra.
 Qed.
 
-(* 9223372036854775808%Z. *)
-Definition bigb_thresh := 1000000000000000000%Z.
+Definition bigb_thresh := 9223372036854775808%Z.
 Lemma step1_div_longu_correct_anyb2 :
     forall a b,
     (1 < Int64.unsigned b <= bigb_thresh)%Z ->
-- 
cgit