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.
---
 interp/notation_term.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 908455bd05..c6ddd9ac95 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -44,6 +44,7 @@ type notation_constr =
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
   | NInt of Uint63.t
+  | NFloat of Float64.t
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted
-- 
cgit v1.2.3