diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-05-04 11:51:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-05-04 11:51:12 +0200 |
| commit | f070949a7559675af3e551e16e5cae95af5d4285 (patch) | |
| tree | 0093b0a2bcf427ad7e54275a54a2e99629d8d091 | |
| parent | 2cccb81243c5b2f45085634ffe070adc1ebb0c1b (diff) | |
| download | compcert-f070949a7559675af3e551e16e5cae95af5d4285.tar.gz compcert-f070949a7559675af3e551e16e5cae95af5d4285.zip | |
Do not use the list notation `[]`
The rest of the code base uses `nil`, so let's be consistent.
Also, this avoids depending on `Import ListNotations`.
| -rw-r--r-- | lib/Floats.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..00d00a57 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -223,10 +223,10 @@ Definition cons_pl (x: float) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x nil)). Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y nil))). (** For fused multiply-add, the order in which arguments are examined to select a NaN payload varies across platforms. E.g. in [fma x y z], @@ -236,7 +236,7 @@ Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c nil)))). (** One last wrinkle for fused multiply-add: [fma zero infinity nan] can return either the quiesced [nan], or the default NaN arising out @@ -248,7 +248,7 @@ Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z @@ -1011,20 +1011,20 @@ Definition cons_pl (x: float32) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x nil)). Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y nil))). Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c nil)))). Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z |