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/typeops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index c71a0e0ca4..ae816fe26e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -120,6 +120,9 @@ val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit
 val type_of_int : env -> types
 val judge_of_int : env -> Uint63.t -> unsafe_judgment
 
+val type_of_float : env -> types
+val judge_of_float : env -> Float64.t -> unsafe_judgment
+
 val type_of_prim_type : env -> CPrimitives.prim_type -> types
 val type_of_prim : env -> CPrimitives.t -> types
 
-- 
cgit v1.2.3