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/nativelambda.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 70b3beb2dc..301773143c 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -580,6 +580,8 @@ let rec lambda_of_constr cache env sigma c =
 
   | Int i -> Luint i
 
+  | Float _ -> assert false  (* native computed for primitive float not yet implemented *)
+
 and lambda_of_app cache env sigma f args =
   match kind f with
   | Const (_kn,_u as c) ->
-- 
cgit v1.2.3