diff options
| -rw-r--r-- | kvx/FPDivision64.v | 2 |
1 files changed, 0 insertions, 2 deletions
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. |