Revert "Added semantic for AArch64 built-in function fmin/fmax."

This reverts commit c770672.

This is not the actual semantics of the AArch64 fmin and fmax instructions.
(NaN behavior; -0.0 treated as less than +0.0.)

Author: xavierleroy

aarch64/Builtins1.v

@@ -19,35 +19,15 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type :=
-  | BI_fmin
-  | BI_fmax.
+Inductive platform_builtin : Type := .
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-    ("__builtin_fmin", BI_fmin)
-  :: ("__builtin_fmax", BI_fmax)
-  :: nil.
+  nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with
-  | BI_fmin | BI_fmax =>
-      mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default
-  end.
+  match b with end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with
-  | BI_fmin =>
-      mkbuiltin_n2t Tfloat Tfloat Tfloat
-        (fun f1 f2 => match Float.compare f1 f2 with
-                      | Some Eq | Some Lt => f1
-                      | Some Gt | None => f2
-                      end)
-  | BI_fmax =>
-      mkbuiltin_n2t Tfloat Tfloat Tfloat
-        (fun f1 f2 => match Float.compare f1 f2 with
-                      | Some Eq | Some Gt => f1
-                      | Some Lt | None => f2
-                      end)
-  end.
+  match b with end.