diff options
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index eeb578d0..441345bf 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -24,7 +24,6 @@ Inductive platform_builtin : Type := | BI_fmax | BI_fminf | BI_fmaxf -| BI_fabsf | BI_fma | BI_fmaf. @@ -35,7 +34,6 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmax", BI_fmax) :: ("__builtin_fminf", BI_fminf) :: ("__builtin_fmaxf", BI_fmaxf) - :: ("__builtin_fabsf", BI_fabsf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) :: nil. @@ -46,8 +44,6 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fminf | BI_fmaxf => mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default - | BI_fabsf => - mksignature (Tsingle :: nil) Tsingle cc_default | BI_fma => mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => @@ -60,7 +56,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max | BI_fminf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.min | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max - | BI_fabsf => mkbuiltin_n1t Tsingle Tsingle Float32.abs | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma end. |