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.

4 files changed, 7 insertions, 4 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 23d066df58..46a80239cf 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
 let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
 let mkInt i = of_kind (Int i)
+let mkFloat f = of_kind (Float f)
 
 let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstRef c -> mkConstU (c,u)
@@ -334,7 +335,7 @@ let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2afce38db7..90f50b764c 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
+val mkFloat : Float64.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 89c2fade62..b850f38b4d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
   in
   hdrec c
 
@@ -165,6 +165,7 @@ let hdchar env sigma c =
     | Evar _ (* We could do better... *)
     | Meta _ | Case (_, _, _, _) -> "y"
     | Int _ -> "i"
+    | Float _ -> "f"
   in
   hdrec 0 c
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 2ab2f60421..90fa8546ce 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c =
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c
+    | Construct _ | Int _ | Float _) -> c
   | Cast (b,k,t) -> 
     let b' = f l b in 
     let t' = f l t in
@@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> cstr
+    | Construct _ | Int _ | Float _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in