From c9cf844e7bdb4eb8bf1b7259f9edd6116629d201 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 1 Oct 2020 20:44:30 +0200
Subject: Remove floating-point comparison operators as they are no longer
 needed.

---
 kernel/byterun/coq_float64.c | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_float64.c b/kernel/byterun/coq_float64.c
index 5ddddbf650..ebbfe35fa6 100644
--- a/kernel/byterun/coq_float64.c
+++ b/kernel/byterun/coq_float64.c
@@ -15,15 +15,6 @@
 
 #include "coq_values.h"
 
-#define DECLARE_FREL(name, e)                                           \
-  int coq_##name(double x, double y) {                                  \
-    return e;                                                           \
-  }                                                                     \
-                                                                        \
-  value coq_##name##_byte(value x, value y) {                           \
-    return coq_##name(Double_val(x), Double_val(y));                    \
-  }
-
 #define DECLARE_FBINOP(name, e)                                         \
   double coq_##name(double x, double y) {                               \
     return e;                                                           \
@@ -42,9 +33,6 @@
     return caml_copy_double(coq_##name(Double_val(x)));                 \
   }
 
-DECLARE_FREL(feq, x == y)
-DECLARE_FREL(flt, x < y)
-DECLARE_FREL(fle, x <= y)
 DECLARE_FBINOP(fmul, x * y)
 DECLARE_FBINOP(fadd, x + y)
 DECLARE_FBINOP(fsub, x - y)
-- 
cgit v1.2.3