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.

1 files changed, 21 insertions, 0 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 52bd9a6ada..000f6125a6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1403,6 +1403,27 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
     check_type_cte 1;
     check_name 2 "Gt";
     check_type_cte 2
+  | CPrimitives.PIT_option ->
+    check_nconstr 2;
+    check_name 0 "Some";
+    let cSome = ob.mind_user_lc.(0) in
+    let s = Pp.str "the first option constructor (Some) has a wrong type" in
+    begin match Term.decompose_prod cSome with
+      | ([_,v;_,_V], codom) ->
+        check_if (is_Type _V) s;
+        check_if (Constr.equal v (mkRel 1)) s;
+        check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s
+      | _ -> check_if false s
+    end;
+    check_name 1 "None";
+    let cNone = ob.mind_user_lc.(1) in
+    let s = Pp.str "the second option constructor (None) has a wrong type" in
+    begin match Term.decompose_prod cNone with
+      | ([_,_V], codom) ->
+        check_if (is_Type _V) s;
+        check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s
+      | _ -> check_if false s
+    end
 
 let register_inductive ind prim senv =
   check_register_ind ind prim senv.env;