diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:41:37 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:41:37 +0100 |
| commit | ddc5dbba8f6e6eaf0bb08a401a679e6c8fdfe07b (patch) | |
| tree | 56f13f87a100ed84914d3ff66ce19b12e5a50011 /kvx | |
| parent | ed7f246f082cc92283e773b6b6b4eb4828a3c2ca (diff) | |
| download | compcert-kvx-ddc5dbba8f6e6eaf0bb08a401a679e6c8fdfe07b.tar.gz compcert-kvx-ddc5dbba8f6e6eaf0bb08a401a679e6c8fdfe07b.zip | |
removing admits
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 7790d31e..b23e3e57 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -461,11 +461,11 @@ Proof. unfold div_approx_reals. fold a' b' prod' prod_r. unfold Int64.mul. - rewrite Int64.unsigned_repr by admit. - rewrite Int64.unsigned_repr by admit. + rewrite Int64.unsigned_repr by (cbn; lia). + rewrite Int64.unsigned_repr by (cbn; lia). unfold Int64.sub. - rewrite Int64.unsigned_repr by admit. - rewrite Int64.unsigned_repr by admit. + rewrite Int64.unsigned_repr by (cbn; lia). + rewrite Int64.unsigned_repr by (cbn; nia). case Z.ltb_spec; intro CMP. - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true by admit. cbn. |