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/typeops.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9913772f2..3e79b174b8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -241,16 +241,16 @@ let type_of_prim env t =
     | Some ((ind,_),_,_) -> Constr.mkInd ind
     | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
   in
+  let f_compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_cmp with
+    | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
+  in
   let pair_ty fst_ty snd_ty =
     match env.retroknowledge.Retroknowledge.retro_pair with
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
     | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
   in
-  let option_ty ty =
-    match env.retroknowledge.Retroknowledge.retro_option with
-    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
-    | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
-  in
   let carry_ty int_ty =
     match env.retroknowledge.Retroknowledge.retro_carry with
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -265,7 +265,7 @@ let type_of_prim env t =
     | PIT_carry, t -> carry_ty (tr_prim_type t)
     | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
     | PIT_cmp, () -> compare_ty ()
-    | PIT_option, () -> option_ty (compare_ty ()) in
+    | PIT_f_cmp, () -> f_compare_ty () in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
-- 
cgit v1.2.3