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.

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index a84353bdc6..e897be6141 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -24,7 +24,9 @@ type retroknowledge = {
     retro_pair : constructor option;
     retro_cmp : (constructor * constructor * constructor) option;
                     (* Eq, Lt, Gt *)
-    retro_option : (constructor * constructor) option; (* Some, None *)
+    retro_f_cmp : (constructor * constructor * constructor * constructor)
+                  option;
+                  (* FEq, FLt, FGt, FNotComparable *)
     retro_refl : constructor option;
 }
 
@@ -35,7 +37,7 @@ let empty = {
     retro_carry = None;
     retro_pair = None;
     retro_cmp = None;
-    retro_option = None;
+    retro_f_cmp = None;
     retro_refl = None;
 }