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.
---
 engine/eConstr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2afce38db7..90f50b764c 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
+val mkFloat : Float64.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
-- 
cgit v1.2.3