From b11fd5400cb042f4b0727e08d2fa53929092f74c Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 7 Jan 2022 15:32:51 +0100
Subject: progress

---
 kvx/FPDivision64.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index a44de06e..851a6cc4 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -205,5 +205,8 @@ Proof.
     set (r_b_d := B2R 53 1024 b_d) in *.
     gappa.
   }
+  destruct C7 as (C7R & C7F & _).
+
+  split. assumption.
   
 Admitted.
-- 
cgit