diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:48:14 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:48:14 +0100 |
| commit | 784976ab246e87657c483388edac46208c4c283b (patch) | |
| tree | 053e535a138307d3823adcae9318f42e629b2270 /kvx | |
| parent | 16b875d816a0b62037f4ffd1a0233f516529e5ec (diff) | |
| download | compcert-kvx-784976ab246e87657c483388edac46208c4c283b.tar.gz compcert-kvx-784976ab246e87657c483388edac46208c4c283b.zip | |
simplify proof
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. |