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.
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ec32c83670..c86b70c78e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1847,7 +1847,7 @@ let vernac_register qid r =
         | "ind_carry" -> CPrimitives.(PIE PIT_carry)
         | "ind_pair" -> CPrimitives.(PIE PIT_pair)
         | "ind_cmp" -> CPrimitives.(PIE PIT_cmp)
-        | "ind_option" -> CPrimitives.(PIE PIT_option)
+        | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp)
         | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
       in
       match gr with
-- 
cgit v1.2.3