Revert "Added semantics for fmin/fmax for RISC-V"

This reverts commit c7daf17.

This is not the actual behavior of the fmin/fmax RISC-V instructions.
(-0.0 is to be treated as less than +0.0.)

riscV/Builtins1.v

@@ -19,47 +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.
-
-(* Canonical NaN as defined in the RISC-V ISA, all expontent bits one, sign bit
-   zero and quiet bit one. *)
-Definition canonical_nan := Float.of_bits (Int64.repr 9221120237041090560).
-
-(* NaN handling as described for fmin/fmax by the RISC-V Isa. If one of the
-   parameters is NaN, the other one is returned. Otherwise the canonical NaN
-   value is returned. *)
-Definition nan_handling (f1 f2: float) : float :=
-  if negb (Binary.is_nan _ _ f1) then f1
-  else if negb (Binary.is_nan _ _ f2) then f2
-  else canonical_nan.
+  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 => nan_handling f1 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 => nan_handling f1 f2
-                      end)
-  end.
+  match b with end.