diff options
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index a7ed34fc..0ba9a39f 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -593,9 +593,6 @@ Proof. rewrite Int64.signed_repr by (cbn ; lia). unfold Int64.loword. rewrite Int64.unsigned_repr. reflexivity. - fold prod' in NEAR. - fold a' in NEAR. - fold b' in NEAR. split. 2: cbn; lia. replace (prod_r + (-1)) with (prod_r - 1) by lia. |