From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 14:31:37 +0200
Subject: 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.
---
 kernel/retroknowledge.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/retroknowledge.ml')

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;
 }
 
-- 
cgit v1.2.3