From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 13 Jul 2018 16:22:35 +0200
Subject: Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
---
 kernel/uint63_63.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/uint63_63.ml')

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..4c9377b628 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,6 +27,9 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let of_float = int_of_float
+let to_float i = Int64.to_float (to_uint64 i)
+
 let hash i = i
 [@@ocaml.inline always]
 
-- 
cgit v1.2.3