Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

3 files changed, 28 insertions, 6 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 98fe436a22..5822a1a586 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -248,6 +248,7 @@ let build_beq_scheme mode kn =
         | Meta _  -> raise (EqUnknown "meta-variable")
         | Evar _  -> raise (EqUnknown "existential variable")
         | Int _ -> raise (EqUnknown "int")
+        | Float _ -> raise (EqUnknown "float")
     in
       aux t
   in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1387ca4675..b4c0a33585 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -244,7 +244,8 @@ GRAMMAR EXTEND Gram
    ;
 
    register_type_token:
-     [ [ "#int63_type" -> { CPrimitives.PT_int63 } ] ]
+     [ [ "#int63_type" -> { CPrimitives.PT_int63 }
+       | "#float64_type" -> { CPrimitives.PT_float64 } ] ]
    ;
 
    register_prim_token:
@@ -272,6 +273,24 @@ GRAMMAR EXTEND Gram
        | "#int63_lt" -> { CPrimitives.Int63lt }
        | "#int63_le" -> { CPrimitives.Int63le }
        | "#int63_compare" -> { CPrimitives.Int63compare }
+       | "#float64_opp" -> { CPrimitives.Float64opp }
+       | "#float64_abs" -> { CPrimitives.Float64abs }
+       | "#float64_eq" -> { CPrimitives.Float64eq }
+       | "#float64_lt" -> { CPrimitives.Float64lt }
+       | "#float64_le" -> { CPrimitives.Float64le }
+       | "#float64_compare" -> { CPrimitives.Float64compare }
+       | "#float64_classify" -> { CPrimitives.Float64classify }
+       | "#float64_add" -> { CPrimitives.Float64add }
+       | "#float64_sub" -> { CPrimitives.Float64sub }
+       | "#float64_mul" -> { CPrimitives.Float64mul }
+       | "#float64_div" -> { CPrimitives.Float64div }
+       | "#float64_sqrt" -> { CPrimitives.Float64sqrt }
+       | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 }
+       | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa }
+       | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp }
+       | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp }
+       | "#float64_next_up" -> { CPrimitives.Float64next_up }
+       | "#float64_next_down" -> { CPrimitives.Float64next_down }
        ] ]
     ;
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ade291918e..6dfba02ae9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1844,11 +1844,13 @@ let vernac_register qid r =
     if DirPath.equal (dirpath_of_string "kernel") ns then begin
       if Global.sections_are_opened () then
         user_err Pp.(str "Registering a kernel type is not allowed in sections");
-      let pind = match Id.to_string id with
-        | "ind_bool" -> CPrimitives.PIT_bool
-        | "ind_carry" -> CPrimitives.PIT_carry
-        | "ind_pair" -> CPrimitives.PIT_pair
-        | "ind_cmp" -> CPrimitives.PIT_cmp
+      let CPrimitives.PIE pind = match Id.to_string id with
+        | "ind_bool" -> CPrimitives.(PIE PIT_bool)
+        | "ind_carry" -> CPrimitives.(PIE PIT_carry)
+        | "ind_pair" -> CPrimitives.(PIE PIT_pair)
+        | "ind_cmp" -> CPrimitives.(PIE PIT_cmp)
+        | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp)
+        | "ind_f_class" -> CPrimitives.(PIE PIT_f_class)
         | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
       in
       match gr with