From fa79debdca4121f2435750b8090e83b541887979 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 09:35:23 +0100
Subject: progress

---
 kvx/FPDivision64.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 0dfa9882..8d40e88e 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1145,7 +1145,7 @@ Proof.
     lia.
   } 
   destruct (BofZ_exact 53 1024 re re (Int64.signed a) SILLY) as (C1R & C1F & C1S).
-  fold a' in C1R.
+  fold a' in C1R, C1F, C1S.
   pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE (BofZ 53 1024 re re a') f) as C2.
   rewrite Rlt_bool_true in C2 ; cycle 1.
   { clear C2.
@@ -1160,7 +1160,14 @@ Proof.
     unfold smalla_thresh in *.
     gappa.
   }
-  cbn.
+  rewrite C0F in C2.
+  rewrite C1R in C2.
+  rewrite C1F in C2.
+  rewrite C1S in C2.
+  cbn in C2.
+  destruct C2 as (C2R & C2F & _).
+  rewrite C2R.
+  admit.
 Admitted.
 
 Definition step2_div_long' a b :=
-- 
cgit