diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:19:17 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:19:17 +0100 |
| commit | e88eb7bdf74f68c4577477650332240dabfee88e (patch) | |
| tree | d66cd8179b70466726e3d122d6d09e0a36eda9cc /kvx | |
| parent | 18bbbf846dcfbc4454ccbbf0ff837024bcd383e3 (diff) | |
| download | compcert-kvx-e88eb7bdf74f68c4577477650332240dabfee88e.tar.gz compcert-kvx-e88eb7bdf74f68c4577477650332240dabfee88e.zip | |
better
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 4ea3f5a3..6fd7e14c 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -411,7 +411,7 @@ Proof. destruct C1 as (C1E & C1F & _). rewrite C1F. cbn. - assert(prod'_range : (0 <= prod' <= 4294967296)%R). + assert(prod'_range : (0 <= prod' <= 17179869181/4)%R). { rewrite C1E. apply Rabs_def2b in inv_b_correct. |