From 784976ab246e87657c483388edac46208c4c283b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Dec 2021 12:48:14 +0100 Subject: simplify proof --- kvx/FPDivision.v | 3 --- 1 file changed, 3 deletions(-) (limited to 'kvx') 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. -- cgit