diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 12:30:16 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 12:30:16 +0200 |
| commit | 344fd96e0690ff4809623198baeee823132f7219 (patch) | |
| tree | 59df0a1cba62fe24d2b5a70ef7b9da5e1321c59a /mppa_k1c/ExtFloats.v | |
| parent | cfc681ae18c59f4a19143a7245be23eb6a4045a0 (diff) | |
| download | compcert-kvx-344fd96e0690ff4809623198baeee823132f7219.tar.gz compcert-kvx-344fd96e0690ff4809623198baeee823132f7219.zip | |
use finvw
Diffstat (limited to 'mppa_k1c/ExtFloats.v')
| -rw-r--r-- | mppa_k1c/ExtFloats.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v index b2fc6581..d9b9d3a6 100644 --- a/mppa_k1c/ExtFloats.v +++ b/mppa_k1c/ExtFloats.v @@ -32,7 +32,8 @@ Definition max (x : float32) (y : float32) : float32 := | Some Lt | None => y end. +Definition one := Float32.of_int (Int.repr (1%Z)). Definition inv (x : float32) : float32 := - Float32.div (Float32.of_int (Int.repr (1%Z))) x. + Float32.div one x. End ExtFloat32. |