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.
---
 plugins/funind/functional_principles_proofs.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7be049269c..6db0a1119b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -692,13 +692,14 @@ let build_proof
               end
           | Cast(t,_,_) ->
               build_proof do_finalize {dyn_infos with info = t} g
-          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
               do_finalize dyn_infos g
           | App(_,_) ->
               let f,args = decompose_app sigma dyn_infos.info in
               begin
                 match EConstr.kind sigma f with
-      | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Float _ -> user_err Pp.(str "float cannot be applied")
                   | App _ -> assert false (* we have collected all the app in decompose_app *)
                   | Proj _ -> assert false (*FIXME*)
                   | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
-- 
cgit v1.2.3