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

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

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8abccabae6..5f54bad598 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -115,6 +115,7 @@ let change_vars =
       | GSort _ as x -> x
       | GHole _ as x -> x
       | GInt _ as x -> x
+      | GFloat _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
@@ -295,6 +296,7 @@ let rec alpha_rt excluded rt =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
     | GInt _
+    | GFloat _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
@@ -354,7 +356,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
-    | GInt _ -> false
+    | GInt _ | GFloat _ -> false
     ) x
   and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -447,6 +449,7 @@ let replace_var_by_term x_id term =
       | GSort _
       | GHole _ as rt -> rt
       | GInt _ as rt -> rt
+      | GFloat _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -529,7 +532,7 @@ let expand_as =
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map = DAst.map (function
-      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt
       | GVar id as rt ->
 	  begin
 	    try
-- 
cgit v1.2.3