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, 14 insertions, 10 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 520bcd6b41..bac13a0bd7 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -241,8 +241,6 @@ module VNativeEntries =
 
     let float_ty env = VAL(0, mkConst @@ get_float_type env)
 
-    let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env)
-
     let mkCarry env b e =
       let (c0,c1) = get_carry_constructors env in
       CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|])
@@ -270,15 +268,21 @@ module VNativeEntries =
       let (_eq,_lt,gt) = get_cmp_constructors env in
       CONSTR(Univ.in_punivs gt, [||])
 
-    let mkSomeCmp env v =
-      let cmp_ty = cmp_ty env in
-      let (some,_none) = get_option_constructors env in
-      CONSTR(Univ.in_punivs some, [|cmp_ty;v|])
+    let mkFLt env =
+      let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs lt, [||])
+
+    let mkFEq env =
+      let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs eq, [||])
+
+    let mkFGt env =
+      let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs gt, [||])
 
-    let mkNoneCmp env =
-      let cmp_ty = cmp_ty env in
-      let (_some,none) = get_option_constructors env in
-      CONSTR(Univ.in_punivs none, [|cmp_ty|])
+    let mkFNotComparable env =
+      let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs nc, [||])
   end
 
 module VredNative = RedNative(VNativeEntries)