Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.

2 files changed, 8 insertions, 9 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 55b973dcdb..74edd79872 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1551,19 +1551,16 @@ value coq_interprete
         x = Double_val(accu);
         y = Double_val(*sp++);
         if(x < y) {
-          Alloc_small(accu, 1, coq_tag_Some);
-          Field(accu, 0) = coq_Lt;
+          accu = coq_FLt;
         }
         else if(x > y) {
-          Alloc_small(accu, 1, coq_tag_Some);
-          Field(accu, 0) = coq_Gt;
+          accu = coq_FGt;
         }
         else if(x == y) {
-          Alloc_small(accu, 1, coq_tag_Some);
-          Field(accu, 0) = coq_Eq;
+          accu = coq_FEq;
         }
         else { // nan value
-          accu = coq_None;
+          accu = coq_FNotComparable;
         }
         Next;
       }
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index fa51b2d31f..c79a8f1b4f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -42,8 +42,10 @@
 #define coq_Eq Val_int(0)
 #define coq_Lt Val_int(1)
 #define coq_Gt Val_int(2)
-#define coq_tag_Some 1
-#define coq_None Val_int(0)
+#define coq_FEq Val_int(0)
+#define coq_FLt Val_int(1)
+#define coq_FGt Val_int(2)
+#define coq_FNotComparable Val_int(3)
 
 #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */