From 2bbe86d4efe2ae08444359008798c12adf0c9b60 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Jan 2022 22:39:55 +0100 Subject: some progress --- kvx/FPDivision64.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e4f883e7..3685f601 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1428,7 +1428,6 @@ Proof. replace (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring. set (q'' := (ZnearestE q')) in *. - Check Int64.sub_signed. fold a'. rewrite int64_mul_signed_unsigned. rewrite q_SIGNED. @@ -1706,7 +1705,6 @@ Proof. replace (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring. set (q'' := (ZnearestE q')) in *. - Check Int64.sub_signed. fold a'. rewrite int64_mul_signed_unsigned. rewrite q_SIGNED. -- cgit