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

(limited to 'kernel/retypeops.ml')

diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index f398e6a5da..5c15257511 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -60,7 +60,7 @@ let rec relevance_of_fterm env extra lft f =
       | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
       | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
       | FFlex key -> relevance_of_flex env extra lft key
-      | FInt _ -> Sorts.Relevant
+      | FInt _ | FFloat _ -> Sorts.Relevant
       | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
       | FConstruct (c,_) -> relevance_of_constructor env c
       | FApp (f, _) -> relevance_of_fterm env extra lft f
@@ -105,7 +105,7 @@ and relevance_of_term_extra env extra lft subs c =
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
-  | Int _ -> Sorts.Relevant
+  | Int _ | Float _ -> Sorts.Relevant
 
   | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *)
 
-- 
cgit v1.2.3