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

48 files changed, 1653 insertions, 175 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 0865487c98..931b509f48 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -44,6 +44,7 @@ void init_arity () {
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
     arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
     arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+    arity[LTFLOAT]=arity[LEFLOAT]=
     arity[ISINT]=arity[AREINT2]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
@@ -63,7 +64,15 @@ void init_arity () {
     arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
     arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
     arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
-    arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1;
+    arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
+    arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
+    arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
+    arity[CHECKCLASSIFYFLOAT]=
+    arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
+    arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
+    arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
+    arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=
+    arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
   arity[PROJ]=2;
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h
new file mode 100644
index 0000000000..c41079c8ff
--- /dev/null
+++ b/kernel/byterun/coq_float64.h
@@ -0,0 +1,48 @@
+#ifndef _COQ_FLOAT64_
+#define _COQ_FLOAT64_
+
+#include <math.h>
+
+#define DECLARE_FREL(name, e)                                           \
+  int coq_##name(double x, double y) {                                  \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x, value y) {                           \
+    return coq_##name(Double_val(x), Double_val(y));                    \
+  }
+
+#define DECLARE_FBINOP(name, e)                                         \
+  double coq_##name(double x, double y) {                               \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x, value y) {                           \
+    return caml_copy_double(coq_##name(Double_val(x), Double_val(y)));  \
+  }
+
+#define DECLARE_FUNOP(name, e)                                          \
+  double coq_##name(double x) {                                         \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x) {                                    \
+    return caml_copy_double(coq_##name(Double_val(x)));                 \
+  }
+
+DECLARE_FREL(feq, x == y)
+DECLARE_FREL(flt, x < y)
+DECLARE_FREL(fle, x <= y)
+DECLARE_FBINOP(fmul, x * y)
+DECLARE_FBINOP(fadd, x + y)
+DECLARE_FBINOP(fsub, x - y)
+DECLARE_FBINOP(fdiv, x / y)
+DECLARE_FUNOP(fsqrt, sqrt(x))
+DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
+DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
+
+value coq_is_double(value x) {
+  return Val_long(Is_double(x));
+}
+
+#endif /* _COQ_FLOAT64_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 4b45608ae5..ca1308696c 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -17,11 +17,13 @@
 #include <signal.h>
 #include <stdint.h>
 #include <caml/memory.h>
+#include <math.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h" 
 #include "coq_values.h" 
+#include "coq_float64.h"
 
 #ifdef ARCH_SIXTYFOUR
 #include "coq_uint63_native.h"
@@ -167,38 +169,34 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #endif
 #endif
 
-#define CheckInt1() do{                            \
-    if (Is_uint63(accu)) pc++;			   \
+#define CheckPrimArgs(cond, apply_lbl) do{         \
+    if (cond) pc++;                                \
     else{					   \
       *--sp=accu;				   \
       accu = Field(coq_global_data, *pc++);	   \
-      goto apply1;				   \
-    }						   \
-  }while(0)
-
-#define CheckInt2() do{    			   \
-    if (Is_uint63(accu) && Is_uint63(sp[0])) pc++;	   \
-    else{					   \
-      *--sp=accu;				   \
-      accu = Field(coq_global_data, *pc++);	   \
-      goto apply2;				   \
+      goto apply_lbl;                              \
     }						   \
   }while(0)
 
-
-
-#define CheckInt3() do{						      \
-    if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++;     \
-    else{							      \
-      *--sp=accu;						      \
-      accu = Field(coq_global_data, *pc++);			      \
-      goto apply3;						      \
-    }								      \
-  }while(0)
+#define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1)
+#define CheckInt2() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]), apply2)
+#define CheckInt3() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]) \
+                                                  && Is_uint63(sp[1]), apply3)
+#define CheckFloat1() CheckPrimArgs(Is_double(accu), apply1)
+#define CheckFloat2() CheckPrimArgs(Is_double(accu) && Is_double(sp[0]), apply2)
 
 #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
 #define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
 
+/* Beware: we cannot use caml_copy_double here as it doesn't use
+   Alloc_small, hence doesn't protect the stack via
+   Setup_for_gc/Restore_after_gc. */
+#define Coq_copy_double(val) do{                   \
+  double Coq_copy_double_f__ = (val);              \
+  Alloc_small(accu, Double_wosize, Double_tag);    \
+  Store_double_val(accu, Coq_copy_double_f__);     \
+  }while(0);
+
 #define Swap_accu_sp do{                        \
     value swap_accu_sp_tmp__ = accu;            \
     accu = *sp;                                 \
@@ -1533,6 +1531,206 @@ value coq_interprete
       }
 
 
+      Instruct (CHECKOPPFLOAT) {
+        print_instr("CHECKOPPFLOAT");
+        CheckFloat1();
+        Coq_copy_double(-Double_val(accu));
+        Next;
+      }
+
+      Instruct (CHECKABSFLOAT) {
+        print_instr("CHECKABSFLOAT");
+        CheckFloat1();
+        Coq_copy_double(fabs(Double_val(accu)));
+        Next;
+      }
+
+      Instruct (CHECKEQFLOAT) {
+        print_instr("CHECKEQFLOAT");
+        CheckFloat2();
+        accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
+      Instruct (CHECKLTFLOAT) {
+        print_instr("CHECKLTFLOAT");
+        CheckFloat2();
+      }
+      Instruct (LTFLOAT) {
+        print_instr("LTFLOAT");
+        accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
+      Instruct (CHECKLEFLOAT) {
+        print_instr("CHECKLEFLOAT");
+        CheckFloat2();
+      }
+      Instruct (LEFLOAT) {
+        print_instr("LEFLOAT");
+        accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
+      Instruct (CHECKCOMPAREFLOAT) {
+        double x, y;
+        print_instr("CHECKCOMPAREFLOAT");
+        CheckFloat2();
+        x = Double_val(accu);
+        y = Double_val(*sp++);
+        if(x < y) {
+          accu = coq_FLt;
+        }
+        else if(x > y) {
+          accu = coq_FGt;
+        }
+        else if(x == y) {
+          accu = coq_FEq;
+        }
+        else { // nan value
+          accu = coq_FNotComparable;
+        }
+        Next;
+      }
+
+      Instruct (CHECKCLASSIFYFLOAT) {
+        double x;
+        print_instr("CHECKCLASSIFYFLOAT");
+        CheckFloat1();
+        x = Double_val(accu);
+        switch (fpclassify(x)) {
+        case FP_NORMAL:
+          accu = signbit(x) ? coq_NNormal : coq_PNormal;
+          break;
+        case FP_SUBNORMAL:
+          accu = signbit(x) ? coq_NSubn : coq_PSubn;
+          break;
+        case FP_ZERO:
+          accu = signbit(x) ? coq_NZero : coq_PZero;
+          break;
+        case FP_INFINITE:
+          accu = signbit(x) ? coq_NInf : coq_PInf;
+          break;
+        default:  /* FP_NAN */
+          accu = coq_NaN;
+          break;
+        }
+        Next;
+      }
+
+      Instruct (CHECKADDFLOAT) {
+        print_instr("CHECKADDFLOAT");
+        CheckFloat2();
+        Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++)));
+        Next;
+      }
+
+      Instruct (CHECKSUBFLOAT) {
+        print_instr("CHECKSUBFLOAT");
+        CheckFloat2();
+        Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++)));
+        Next;
+      }
+
+      Instruct (CHECKMULFLOAT) {
+        print_instr("CHECKMULFLOAT");
+        CheckFloat2();
+        Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++)));
+        Next;
+      }
+
+      Instruct (CHECKDIVFLOAT) {
+        print_instr("CHECKDIVFLOAT");
+        CheckFloat2();
+        Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++)));
+        Next;
+      }
+
+      Instruct (CHECKSQRTFLOAT) {
+        print_instr("CHECKSQRTFLOAT");
+        CheckFloat1();
+        Coq_copy_double(coq_fsqrt(Double_val(accu)));
+        Next;
+      }
+
+      Instruct (CHECKFLOATOFINT63) {
+        print_instr("CHECKFLOATOFINT63");
+        CheckInt1();
+        Uint63_to_double(accu);
+        Next;
+      }
+
+      Instruct (CHECKFLOATNORMFRMANTISSA) {
+        double f;
+        print_instr("CHECKFLOATNORMFRMANTISSA");
+        CheckFloat1();
+        f = fabs(Double_val(accu));
+        if (f >= 0.5 && f < 1) {
+          Uint63_of_double(ldexp(f, DBL_MANT_DIG));
+        }
+        else {
+          Uint63_of_int(Val_int(0));
+        }
+        Next;
+      }
+
+      Instruct (CHECKFRSHIFTEXP) {
+        int exp;
+        double f;
+        print_instr("CHECKFRSHIFTEXP");
+        CheckFloat1();
+        /* frexp(infinity) incorrectly returns nan on mingw */
+#if defined(__MINGW32__) || defined(__MINGW64__)
+        if (fpclassify(Double_val(accu)) == FP_INFINITE) {
+          f = Double_val(accu);
+        } else
+#endif
+        f = frexp(Double_val(accu), &exp);
+        if (fpclassify(f) == FP_NORMAL) {
+          exp += FLOAT_EXP_SHIFT;
+        }
+        else {
+          exp = 0;
+        }
+        Coq_copy_double(f);
+        *--sp = accu;
+#ifdef ARCH_SIXTYFOUR
+        Alloc_small(accu, 2, coq_tag_pair);
+        Field(accu, 1) = Val_int(exp);
+#else
+        Uint63_of_int(Val_int(exp));
+        *--sp = accu;
+        Alloc_small(accu, 2, coq_tag_pair);
+        Field(accu, 1) = *sp++;
+#endif
+        Field(accu, 0) = *sp++;
+        Next;
+      }
+
+      Instruct (CHECKLDSHIFTEXP) {
+        print_instr("CHECKLDSHIFTEXP");
+        CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2);
+        Swap_accu_sp;
+        Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT));
+        accu = Int_val(accu);
+        Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT));
+        Next;
+      }
+
+      Instruct (CHECKNEXTUPFLOAT) {
+        print_instr("CHECKNEXTUPFLOAT");
+        CheckFloat1();
+        Coq_copy_double(coq_next_up(Double_val(accu)));
+        Next;
+      }
+
+      Instruct (CHECKNEXTDOWNFLOAT) {
+        print_instr("CHECKNEXTDOWNFLOAT");
+        CheckFloat1();
+        Coq_copy_double(coq_next_down(Double_val(accu)));
+        Next;
+      }
+
 /* Debugging and machine control */
 
       Instruct(STOP){
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 528cc6fc1f..143a6d098c 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -156,3 +156,18 @@ DECLARE_BINOP(mulc_ml)
     *(h) = Field(uint63_return_value__, 0); \
     accu = Field(uint63_return_value__, 1); \
   }while(0)
+
+DECLARE_UNOP(to_float)
+#define Uint63_to_double(x) CALL_UNOP(to_float, x)
+
+DECLARE_UNOP(of_float)
+#define Uint63_of_double(f) do{ \
+  Coq_copy_double(f); \
+  CALL_UNOP(of_float, accu); \
+  }while(0)
+
+DECLARE_UNOP(of_int)
+#define Uint63_of_int(x) CALL_UNOP(of_int, x)
+
+DECLARE_BINOP(to_int_min)
+#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 9fbd3f83d8..5be7587091 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -138,3 +138,26 @@ value uint63_div21(value xh, value xl, value y, value* ql) {
   }
 }
 #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))
+
+#define Uint63_to_double(x) Coq_copy_double((double) uint63_of_value(x))
+
+double coq_uint63_to_float(value x) {
+  return (double) uint63_of_value(x);
+}
+
+value coq_uint63_to_float_byte(value x) {
+  return caml_copy_double(coq_uint63_to_float(x));
+}
+
+#define Uint63_of_double(f) do{ \
+  accu = Val_long((uint64_t)(f)); \
+  }while(0)
+
+#define Uint63_of_int(x) (accu = (x))
+
+#define Uint63_to_int_min(n, m) do { \
+  if (uint63_lt((n),(m))) \
+    accu = (n); \
+  else \
+    accu = (m); \
+  }while(0)
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 0cf6ccf532..b027673ac7 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -14,6 +14,8 @@
 #include <caml/alloc.h>
 #include <caml/mlvalues.h>
 
+#include <float.h>
+
 #define Default_tag 0
 #define Accu_tag 0
 
@@ -29,8 +31,9 @@
 /* Les blocs accumulate */
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
+#define Is_double(v) (Tag_val(v) == Double_tag)
 
-/* */
+/* coq values for primitive operations */
 #define coq_tag_C1 2
 #define coq_tag_C0 1
 #define coq_tag_pair 1
@@ -39,5 +42,20 @@
 #define coq_Eq Val_int(0)
 #define coq_Lt Val_int(1)
 #define coq_Gt Val_int(2)
+#define coq_FEq Val_int(0)
+#define coq_FLt Val_int(1)
+#define coq_FGt Val_int(2)
+#define coq_FNotComparable Val_int(3)
+#define coq_PNormal Val_int(0)
+#define coq_NNormal Val_int(1)
+#define coq_PSubn Val_int(2)
+#define coq_NSubn Val_int(3)
+#define coq_PZero Val_int(4)
+#define coq_NZero Val_int(5)
+#define coq_PInf Val_int(6)
+#define coq_NInf Val_int(7)
+#define coq_NaN Val_int(8)
+
+#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
 
 #endif /* _COQ_VALUES_ */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 20bdf28e54..d0145176ea 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,3 +1,16 @@
+; Dune doesn't use configure's output, but it is still necessary for
+; some Coq files to work; will be fixed in the future.
+(rule
+ (targets dune.c_flags)
+ (mode fallback)
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
+
+(env
+ (dev     (c_flags (:include dune.c_flags)))
+ (release (c_flags (:include dune.c_flags)))
+ (ireport (c_flags (:include dune.c_flags))))
+
 (library
  (name byterun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 3fd613e905..72585e5014 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -348,6 +348,7 @@ and fterm =
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
+  | FFloat of Float64.t
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -428,7 +429,7 @@ let rec stack_args_size = function
 let rec lft_fconstr n ft =
   let r = Mark.relevance ft.mark in
   match ft.term with
-    | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft
+    | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft
     | FRel i -> {mark=mark Norm r;term=FRel(i+n)}
     | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
     | FFix(fx,e) ->
@@ -499,6 +500,7 @@ let mk_clos e t =
     | Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
     | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
     | Int i -> {mark = mark Cstr Unknown; term = FInt i}
+    | Float f -> {mark = mark Cstr Unknown; term = FFloat f}
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
         {mark = mark Red Unknown; term = FCLOS(t,e)}
 
@@ -616,6 +618,8 @@ let rec to_constr lfts v =
 
     | FInt i ->
        Constr.mkInt i
+    | FFloat f ->
+        Constr.mkFloat f
 
     | FCLOS (t,env) ->
       if is_subs_id env && is_lift_id lfts then t
@@ -926,7 +930,7 @@ let rec knh info m stk =
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
-       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) ->
+       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) ->
         (m, stk)
 
 (* The same for pure terms *)
@@ -940,7 +944,7 @@ and knht info e t stk =
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
     | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
-    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk)
+    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk)
     | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
     | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
     | Prod (n, t, c) ->
@@ -969,6 +973,11 @@ module FNativeEntries =
       | FInt i -> i
       | _ -> raise Primred.NativeDestKO
 
+    let get_float () e =
+      match [@ocaml.warning "-4"] e.term with
+      | FFloat f -> f
+      | _ -> raise Primred.NativeDestKO
+
     let dummy = {mark = mark Norm KnownR; term = FRel 0}
 
     let current_retro = ref Retroknowledge.empty
@@ -982,6 +991,16 @@ module FNativeEntries =
         fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
       | None -> defined_int := false
 
+    let defined_float = ref false
+    let ffloat = ref dummy
+
+    let init_float retro =
+      match retro.Retroknowledge.retro_float64 with
+      | Some c ->
+        defined_float := true;
+        ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+      | None -> defined_float := false
+
     let defined_bool = ref false
     let ftrue = ref dummy
     let ffalse = ref dummy
@@ -1020,6 +1039,7 @@ module FNativeEntries =
     let fEq = ref dummy
     let fLt = ref dummy
     let fGt = ref dummy
+    let fcmp = ref dummy
 
     let init_cmp retro =
       match retro.Retroknowledge.retro_cmp with
@@ -1027,9 +1047,54 @@ module FNativeEntries =
         defined_cmp := true;
         fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) };
         fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
-        fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }
+        fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) };
+        let (icmp, _) = cEq in
+        fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
       | None -> defined_cmp := false
 
+    let defined_f_cmp = ref false
+    let fFEq = ref dummy
+    let fFLt = ref dummy
+    let fFGt = ref dummy
+    let fFNotComparable = ref dummy
+
+    let init_f_cmp retro =
+      match retro.Retroknowledge.retro_f_cmp with
+      | Some (cFEq, cFLt, cFGt, cFNotComparable) ->
+        defined_f_cmp := true;
+        fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) };
+        fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) };
+        fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) };
+        fFNotComparable :=
+          { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
+      | None -> defined_f_cmp := false
+
+    let defined_f_class = ref false
+    let fPNormal = ref dummy
+    let fNNormal = ref dummy
+    let fPSubn = ref dummy
+    let fNSubn = ref dummy
+    let fPZero = ref dummy
+    let fNZero = ref dummy
+    let fPInf = ref dummy
+    let fNInf = ref dummy
+    let fNaN = ref dummy
+
+    let init_f_class retro =
+      match retro.Retroknowledge.retro_f_class with
+      | Some (cPNormal, cNNormal, cPSubn, cNSubn, cPZero, cNZero,
+              cPInf, cNInf, cNaN) ->
+        defined_f_class := true;
+        fPNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPNormal) };
+        fNNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNNormal) };
+        fPSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPSubn) };
+        fNSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNSubn) };
+        fPZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPZero) };
+        fNZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNZero) };
+        fPInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPInf) };
+        fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) };
+        fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) };
+      | None -> defined_f_class := false
     let defined_refl = ref false
 
     let frefl = ref dummy
@@ -1044,10 +1109,13 @@ module FNativeEntries =
     let init env =
       current_retro := env.retroknowledge;
       init_int !current_retro;
+      init_float !current_retro;
       init_bool !current_retro;
       init_carry !current_retro;
       init_pair !current_retro;
       init_cmp !current_retro;
+      init_f_cmp !current_retro;
+      init_f_class !current_retro;
       init_refl !current_retro
 
     let check_env env =
@@ -1057,6 +1125,10 @@ module FNativeEntries =
       check_env env;
       assert (!defined_int)
 
+    let check_float env =
+      check_env env;
+      assert (!defined_float)
+
     let check_bool env =
       check_env env;
       assert (!defined_bool)
@@ -1073,10 +1145,22 @@ module FNativeEntries =
       check_env env;
       assert (!defined_cmp)
 
+    let check_f_cmp env =
+      check_env env;
+      assert (!defined_f_cmp)
+
+    let check_f_class env =
+      check_env env;
+      assert (!defined_f_class)
+
     let mkInt env i =
       check_int env;
       { mark = mark Cstr KnownR; term = FInt i }
 
+    let mkFloat env f =
+      check_float env;
+      { mark = mark Norm KnownR; term = FFloat f }
+
     let mkBool env b =
       check_bool env;
       if b then !ftrue else !ffalse
@@ -1090,6 +1174,11 @@ module FNativeEntries =
       check_pair env;
       { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) }
 
+    let mkFloatIntPair env f i =
+      check_pair env;
+      check_float env;
+      { mark = mark Cstr KnownR; term = FApp(!fPair, [|!ffloat;!fint;f;i|]) }
+
     let mkLt env =
       check_cmp env;
       !fLt
@@ -1102,6 +1191,57 @@ module FNativeEntries =
       check_cmp env;
       !fGt
 
+    let mkFLt env =
+      check_f_cmp env;
+      !fFLt
+
+    let mkFEq env =
+      check_f_cmp env;
+      !fFEq
+
+    let mkFGt env =
+      check_f_cmp env;
+      !fFGt
+
+    let mkFNotComparable env =
+      check_f_cmp env;
+      !fFNotComparable
+
+    let mkPNormal env =
+      check_f_class env;
+      !fPNormal
+
+    let mkNNormal env =
+      check_f_class env;
+      !fNNormal
+
+    let mkPSubn env =
+      check_f_class env;
+      !fPSubn
+
+    let mkNSubn env =
+      check_f_class env;
+      !fNSubn
+
+    let mkPZero env =
+      check_f_class env;
+      !fPZero
+
+    let mkNZero env =
+      check_f_class env;
+      !fNZero
+
+    let mkPInf env =
+      check_f_class env;
+      !fPInf
+
+    let mkNInf env =
+      check_f_class env;
+      !fNInf
+
+    let mkNaN env =
+      check_f_class env;
+      !fNaN
   end
 
 module FredNative = RedNative(FNativeEntries)
@@ -1164,7 +1304,7 @@ let rec knr info tab m stk =
       (match info.i_cache.i_sigma ev with
           Some c -> knit info tab env c stk
         | None -> (m,stk))
-  | FInt _ ->
+  | FInt _ | FFloat _ ->
     (match [@ocaml.warning "-4"] strip_update_shift_app m stk with
      | (_, _, Zprimitive(op,c,rargs,nargs)::s) ->
        let (rargs, nargs) = skip_native_args (m::rargs) nargs in
@@ -1270,7 +1410,7 @@ and norm_head info tab m =
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
-        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ -> term_of_fconstr m
+        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index cd1de4c834..720f11b8f2 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -115,6 +115,7 @@ type fterm =
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
+  | FFloat of Float64.t
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d854cadd15..9ff7f69203 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -33,6 +33,24 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
+  | Float64compare
+  | Float64classify
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down
 
 let equal (p1 : t) (p2 : t) =
   p1 == p2
@@ -62,6 +80,24 @@ let hash = function
   | Int63lt -> 22
   | Int63le -> 23
   | Int63compare -> 24
+  | Float64opp -> 25
+  | Float64abs -> 26
+  | Float64compare -> 27
+  | Float64classify -> 28
+  | Float64add -> 29
+  | Float64sub -> 30
+  | Float64mul -> 31
+  | Float64div -> 32
+  | Float64sqrt -> 33
+  | Float64ofInt63 -> 34
+  | Float64normfr_mantissa -> 35
+  | Float64frshiftexp -> 36
+  | Float64ldshiftexp -> 37
+  | Float64next_up -> 38
+  | Float64next_down -> 39
+  | Float64eq -> 40
+  | Float64lt -> 41
+  | Float64le -> 42
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -89,6 +125,72 @@ let to_string = function
   | Int63lt -> "lt"
   | Int63le -> "le"
   | Int63compare -> "compare"
+  | Float64opp -> "fopp"
+  | Float64abs -> "fabs"
+  | Float64eq -> "feq"
+  | Float64lt -> "flt"
+  | Float64le -> "fle"
+  | Float64compare -> "fcompare"
+  | Float64classify -> "fclassify"
+  | Float64add -> "fadd"
+  | Float64sub -> "fsub"
+  | Float64mul -> "fmul"
+  | Float64div -> "fdiv"
+  | Float64sqrt -> "fsqrt"
+  | Float64ofInt63 -> "float_of_int"
+  | Float64normfr_mantissa -> "normfr_mantissa"
+  | Float64frshiftexp -> "frshiftexp"
+  | Float64ldshiftexp -> "ldshiftexp"
+  | Float64next_up    -> "next_up"
+  | Float64next_down  -> "next_down"
+
+type prim_type =
+  | PT_int63
+  | PT_float64
+
+type 'a prim_ind =
+  | PIT_bool : unit prim_ind
+  | PIT_carry : prim_type prim_ind
+  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_cmp : unit prim_ind
+  | PIT_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
+
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
+
+type ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : prim_type -> ind_or_type
+
+let types =
+  let int_ty = PITT_type PT_int63 in
+  let float_ty = PITT_type PT_float64 in
+  function
+  | Int63head0 | Int63tail0 -> [int_ty; int_ty]
+  | Int63add | Int63sub | Int63mul
+  | Int63div | Int63mod
+  | Int63lsr | Int63lsl
+  | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+  | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
+     [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)]
+  | Int63mulc | Int63diveucl ->
+     [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
+  | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+  | Int63div21 ->
+     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
+  | Float64opp | Float64abs | Float64sqrt
+  | Float64next_up | Float64next_down -> [float_ty; float_ty]
+  | Float64ofInt63 -> [int_ty; float_ty]
+  | Float64normfr_mantissa -> [float_ty; int_ty]
+  | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+  | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
+  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
+  | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
+  | Float64add | Float64sub | Float64mul
+  | Float64div -> [float_ty; float_ty; float_ty]
+  | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
 
 type arg_kind =
   | Kparam (* not needed for the evaluation of the primitive when it reduces *)
@@ -97,58 +199,32 @@ type arg_kind =
 
 type args_red = arg_kind list
 
-(* Invariant only argument of type int63 or an inductive can
+(* Invariant only argument of type int63, float or an inductive can
    have kind Kwhnf *)
 
-let kind = function
-  | Int63head0 | Int63tail0 -> [Kwhnf]
-
-  | Int63add | Int63sub | Int63mul
-  | Int63div | Int63mod
-  | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC  | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf]
+let arity t = List.length (types t) - 1
 
-  | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf]
-
-let arity = function
-  | Int63head0 | Int63tail0 -> 1
-  | Int63add | Int63sub | Int63mul
-  | Int63div | Int63mod
-  | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le
-  | Int63compare -> 2
-
-  | Int63div21 | Int63addMulDiv -> 3
+let kind t =
+  let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in
+  aux (arity t)
 
 (** Special Entries for Register **)
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
-
-type prim_type =
-  | PT_int63
-
 type op_or_type =
   | OT_op of t
   | OT_type of prim_type
 
-let prim_ind_to_string = function
+let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_bool -> "bool"
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
+  | PIT_f_cmp -> "f_cmp"
+  | PIT_f_class -> "f_class"
 
 let prim_type_to_string = function
   | PT_int63 -> "int63_type"
+  | PT_float64 -> "float64_type"
 
 let op_or_type_to_string = function
   | OT_op op -> to_string op
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 6913371caf..be65ba5305 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -33,6 +33,24 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
+  | Float64compare
+  | Float64classify
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down
 
 val equal : t -> t -> bool
 
@@ -53,18 +71,29 @@ val kind : t -> args_red
 
 (** Special Entries for Register **)
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
-
 type prim_type =
   | PT_int63
+  | PT_float64
+
+type 'a prim_ind =
+  | PIT_bool : unit prim_ind
+  | PIT_carry : prim_type prim_ind
+  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_cmp : unit prim_ind
+  | PIT_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
+
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
 type op_or_type =
   | OT_op of t
   | OT_type of prim_type
 
-val prim_ind_to_string : prim_ind -> string
+val prim_ind_to_string : 'a prim_ind -> string
 val op_or_type_to_string : op_or_type -> string
+
+type ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : prim_type -> ind_or_type
+
+val types : t -> ind_or_type list
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 83d2a58d83..13cc6f7ea4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -528,6 +528,8 @@ let rec compile_lam env cenv lam sz cont =
 
   | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont
 
+  | Lfloat f -> compile_structured_constant cenv (Const_float f) sz cont
+
   | Lproj (p,arg) ->
      compile_lam env cenv arg sz (Kproj p :: cont)
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 76e2515ea7..5e82cef810 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -234,6 +234,24 @@ let check_prim_op = function
   | Int63lt        -> opCHECKLTINT63
   | Int63le        -> opCHECKLEINT63
   | Int63compare   -> opCHECKCOMPAREINT63
+  | Float64opp     -> opCHECKOPPFLOAT
+  | Float64abs     -> opCHECKABSFLOAT
+  | Float64eq      -> opCHECKEQFLOAT
+  | Float64lt      -> opCHECKLTFLOAT
+  | Float64le      -> opCHECKLEFLOAT
+  | Float64compare -> opCHECKCOMPAREFLOAT
+  | Float64classify -> opCHECKCLASSIFYFLOAT
+  | Float64add     -> opCHECKADDFLOAT
+  | Float64sub     -> opCHECKSUBFLOAT
+  | Float64mul     -> opCHECKMULFLOAT
+  | Float64div     -> opCHECKDIVFLOAT
+  | Float64sqrt    -> opCHECKSQRTFLOAT
+  | Float64ofInt63 -> opCHECKFLOATOFINT63
+  | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA
+  | Float64frshiftexp -> opCHECKFRSHIFTEXP
+  | Float64ldshiftexp -> opCHECKLDSHIFTEXP
+  | Float64next_up    -> opCHECKNEXTUPFLOAT
+  | Float64next_down  -> opCHECKNEXTDOWNFLOAT
 
 let emit_instr env = function
   | Klabel lbl -> define_label env lbl
@@ -384,7 +402,8 @@ type to_patch = emitcodes * patches * fv
 (* Substitution *)
 let subst_strcst s sc =
   match sc with
-  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ -> sc
+  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _
+  | Const_float _ -> sc
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_reloc s ri =
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index a764cca354..8c7aa6b17a 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -28,6 +28,7 @@ type lambda =
   | Lint          of int
   | Lmakeblock    of int * lambda array
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of structured_values
   | Lsort         of Sorts.t
   | Lind          of pinductive
@@ -143,6 +144,7 @@ let rec pp_lam lam =
        prlist_with_sep spc pp_lam (Array.to_list args) ++
        str")")
   | Luint i -> str (Uint63.to_string i)
+  | Lfloat f -> str (Float64.to_string f)
   | Lval _ -> str "values"
   | Lsort s -> pp_sort s
   | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
@@ -195,7 +197,8 @@ let shift subst = subs_shft (1, subst)
 
 let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
+  | Lfloat _ -> lam
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
@@ -416,7 +419,8 @@ let rec occurrence k kind lam =
     if n = k then
       if kind then false else raise Not_found
     else kind
-  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> kind
+  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
+  | Lfloat _ -> kind
   | Levar (_, args) ->
     occurrence_args k kind args
   | Lprod(dom, codom) ->
@@ -763,6 +767,7 @@ let rec lambda_of_constr env c =
     Lproj (Projection.repr p,lc)
 
   | Int i -> Luint i
+  | Float f -> Lfloat f
 
 and lambda_of_app env f args =
   match Constr.kind f with
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 1476bb6e45..bd11c2667f 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -21,6 +21,7 @@ type lambda =
   | Lint          of int
   | Lmakeblock    of int * lambda array
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of structured_values
   | Lsort         of Sorts.t
   | Lind          of pinductive
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8375316003..b60b2d6d04 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -104,6 +104,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
+  | Float     of Float64.t
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
@@ -241,6 +242,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with
 (* Constructs a primitive integer *)
 let mkInt i = Int i
 
+(* Constructs a primitive float number *)
+let mkFloat f = Float f
+
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
@@ -446,7 +450,7 @@ let decompose_appvect c =
 
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> acc
+    | Construct _ | Int _ | Float _) -> acc
   | Cast (c,_,t) -> f (f acc c) t
   | Prod (_,t,c) -> f (f acc t) c
   | Lambda (_,t,c) -> f (f acc t) c
@@ -466,7 +470,7 @@ let fold f acc c = match kind c with
 
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f c; f t
   | Prod (_,t,c) -> f t; f c
   | Lambda (_,t,c) -> f t; f c
@@ -486,7 +490,7 @@ let iter f c = match kind c with
 
 let iter_with_binders g f n c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
@@ -512,7 +516,7 @@ let iter_with_binders g f n c = match kind c with
 let fold_constr_with_binders g f n acc c =
   match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> acc
+    | Construct _ | Int _ | Float _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (_na,t,c) -> f (g  n) (f n acc t) c
   | Lambda (_na,t,c) -> f (g  n) (f n acc t) c
@@ -608,7 +612,7 @@ let map_return_predicate_with_full_binders g f l ci p =
 
 let map_gen userview f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c
+    | Construct _ | Int _ | Float _) -> c
   | Cast (b,k,t) ->
       let b' = f b in
       let t' = f t in
@@ -673,7 +677,7 @@ let map = map_gen false
 
 let fold_map f accu c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> accu, c
+    | Construct _ | Int _ | Float _) -> accu, c
   | Cast (b,k,t) ->
       let accu, b' = f accu b in
       let accu, t' = f accu t in
@@ -733,7 +737,7 @@ let fold_map f accu c = match kind c with
 
 let map_with_binders g f l c0 = match kind c0 with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c0
+    | Construct _ | Int _ | Float _) -> c0
   | Cast (c, k, t) ->
     let c' = f l c in
     let t' = f l t in
@@ -810,7 +814,7 @@ let lift n = liftn n 1
 let fold_with_full_binders g f n acc c =
   let open Context.Rel.Declaration in
   match kind c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ -> acc
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
   | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
@@ -852,6 +856,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
   | Int i1, Int i2 -> Uint63.equal i1 i2
+  | Float f1, Float f2 -> Float64.equal f1 f2
   | Sort s1, Sort s2 -> leq_sorts s1 s2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2
@@ -878,7 +883,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
-    | CoFix _ | Int _), _ -> false
+    | CoFix _ | Int _ | Float _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -1055,6 +1060,8 @@ let constr_ord_int f t1 t2 =
     | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
     | Proj _, _ -> -1 | _, Proj _ -> 1
     | Int i1, Int i2 -> Uint63.compare i1 i2
+    | Int _, _ -> -1 | _, Int _ -> 1
+    | Float f1, Float f2 -> Float64.total_compare f1 f2
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -1139,9 +1146,10 @@ let hasheq t1 t2 =
       && array_eqeq tl1 tl2
       && array_eqeq bl1 bl2
     | Int i1, Int i2 -> i1 == i2
+    | Float f1, Float f2 -> Float64.equal f1 f2
     | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
       | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
-      | Fix _ | CoFix _ | Int _), _ -> false
+      | Fix _ | CoFix _ | Int _ | Float _), _ -> false
 
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
@@ -1247,6 +1255,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Int i ->
         let (h,l) = Uint63.to_int2 i in
         (t, combinesmall 18 (combine h l))
+      | Float f -> (t, combinesmall 19 (Float64.hash f))
 
   and sh_rec t =
     let (y, h) = hash_term t in
@@ -1311,6 +1320,7 @@ let rec hash t =
     | Proj (p,c) ->
       combinesmall 17 (combine (Projection.hash p) (hash c))
     | Int i -> combinesmall 18 (Uint63.hash i)
+    | Float f -> combinesmall 19 (Float64.hash f)
 
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash t) acc) 0 t
@@ -1455,3 +1465,4 @@ let rec debug_print c =
            cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++
          str"}")
   | Int i -> str"Int("++str (Uint63.to_string i) ++ str")"
+  | Float i -> str"Float("++str (Float64.to_string i) ++ str")"
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 45ec8a7e64..4f8d682e42 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -76,6 +76,9 @@ val mkVar : Id.t -> constr
 (** Constructs a machine integer *)
 val mkInt : Uint63.t -> constr
 
+(** Constructs a machine float number *)
+val mkFloat : Float64.t -> constr
+
 (** Constructs an patvar named "?n" *)
 val mkMeta : metavariable -> constr
 
@@ -234,6 +237,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
+  | Float     of Float64.t
 
 (** User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 6c9e73b50d..cbffdc731e 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -184,7 +184,16 @@ and eval_to_patch env (buff,pl,fv) =
     | Reloc_proj_name p -> slot_for_proj_name p
   in
   let tc = patch buff pl slots in
-  let vm_env = Array.map (slot_for_fv env) fv in
+  let vm_env =
+    (* Beware, this may look like a call to [Array.map], but it's not.
+       Calling [Array.map f] when the first argument returned by [f]
+       is a float would lead to [vm_env] being an unboxed Double_array
+       (Tag_val = Double_array_tag) whereas eval_tcode expects a
+       regular array (Tag_val = 0).
+       See test-suite/primitive/float/coq_env_double_array.v
+       for an actual instance. *)
+    let a = Array.make (Array.length fv) crazy_val in
+    Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in
   eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
diff --git a/kernel/float64.ml b/kernel/float64.ml
new file mode 100644
index 0000000000..3e36373b77
--- /dev/null
+++ b/kernel/float64.ml
@@ -0,0 +1,159 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* OCaml's float type follows the IEEE 754 Binary64 (double precision)
+   format *)
+type t = float
+
+let is_nan f = f <> f
+let is_infinity f = f = infinity
+let is_neg_infinity f = f = neg_infinity
+
+(* Printing a binary64 float in 17 decimal places and parsing it again
+   will yield the same float. We assume [to_string_raw] is not given a
+   [nan] as input. *)
+let to_string_raw f = Printf.sprintf "%.17g" f
+
+(* OCaml gives a sign to nan values which should not be displayed as
+   all NaNs are considered equal here *)
+let to_string f = if is_nan f then "nan" else to_string_raw f
+let of_string = float_of_string
+
+(* Compiles a float to OCaml code *)
+let compile f =
+  let s =
+    if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity"
+    else Printf.sprintf "%h" f in
+  Printf.sprintf "Float64.of_float (%s)" s
+
+let of_float f = f
+
+let sign f = copysign 1. f < 0.
+
+let opp = ( ~-. )
+let abs = abs_float
+
+type float_comparison = FEq | FLt | FGt | FNotComparable
+
+let eq x y = x = y
+[@@ocaml.inline always]
+
+let lt x y = x < y
+[@@ocaml.inline always]
+
+let le x y = x <= y
+[@@ocaml.inline always]
+
+(* inspired by lib/util.ml; see also #10471 *)
+let pervasives_compare = compare
+
+let compare x y =
+  if x < y then FLt
+  else
+  (
+    if x > y then FGt
+    else
+    (
+      if x = y then FEq
+      else FNotComparable (* NaN case *)
+    )
+  )
+[@@ocaml.inline always]
+
+type float_class =
+  | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+let classify x =
+  match classify_float x with
+  | FP_normal -> if 0. < x then PNormal else NNormal
+  | FP_subnormal -> if 0. < x then PSubn else NSubn
+  | FP_zero -> if 0. < 1. /. x then PZero else NZero
+  | FP_infinite -> if 0. < x then PInf else NInf
+  | FP_nan -> NaN
+[@@ocaml.inline always]
+
+external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul"
+[@@unboxed] [@@noalloc]
+
+external add : float -> float -> float = "coq_fadd_byte" "coq_fadd"
+[@@unboxed] [@@noalloc]
+
+external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub"
+[@@unboxed] [@@noalloc]
+
+external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv"
+[@@unboxed] [@@noalloc]
+
+external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt"
+[@@unboxed] [@@noalloc]
+
+let of_int63 x = Uint63.to_float x
+[@@ocaml.inline always]
+
+let prec = 53
+let normfr_mantissa f =
+  let f = abs f in
+  if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec)
+  else Uint63.zero
+[@@ocaml.inline always]
+
+let eshift = 2101 (* 2*emax + prec *)
+
+(* When calling frexp on a nan or an infinity, the returned value inside
+   the exponent is undefined.
+   Therefore we must always set it to a fixed value (here 0). *)
+let frshiftexp f =
+  match classify_float f with
+  | FP_zero | FP_infinite | FP_nan -> (f, Uint63.zero)
+  | FP_normal | FP_subnormal ->
+    let (m, e) = frexp f in
+    m, Uint63.of_int (e + eshift)
+[@@ocaml.inline always]
+
+let ldshiftexp f e = ldexp f (Uint63.to_int_min e (2 * eshift) - eshift)
+[@@ocaml.inline always]
+
+external next_up : float -> float = "coq_next_up_byte" "coq_next_up"
+[@@unboxed] [@@noalloc]
+
+external next_down : float -> float = "coq_next_down_byte" "coq_next_down"
+[@@unboxed] [@@noalloc]
+
+let equal f1 f2 =
+  match classify_float f1 with
+  | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2)
+  | FP_nan -> is_nan f2
+  | FP_zero -> f1 = f2 && 1. /. f1 = 1. /. f2 (* OCaml consider 0. = -0. *)
+[@@ocaml.inline always]
+
+let hash =
+  (* Hashtbl.hash already considers all NaNs as equal,
+     cf. https://github.com/ocaml/ocaml/commit/aea227fdebe0b5361fd3e1d0aaa42cf929052269
+     and http://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.html *)
+  Hashtbl.hash
+
+let total_compare f1 f2 =
+  (* pervasives_compare considers all NaNs as equal, which is fine here,
+     but also considers -0. and +0. as equal *)
+  if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2)
+  else pervasives_compare f1 f2
+
+let is_float64 t =
+  Obj.tag t = Obj.double_tag
+[@@ocaml.inline always]
+
+(*** Test at runtime that no harmful double rounding seems to
+   be performed with an intermediate 80 bits representation (x87). *)
+let () =
+  let b = ldexp 1. 53 in
+  let s = add 1. (ldexp 1. (-52)) in
+  if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+    failwith "Detected non IEEE-754 compliant architecture (or wrong \
+              rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64.mli b/kernel/float64.mli
new file mode 100644
index 0000000000..2aa9796526
--- /dev/null
+++ b/kernel/float64.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** [t] is currently implemented by OCaml's [float] type.
+
+Beware: NaNs have a sign and a payload, while they should be
+indistinguishable from Coq's perspective. *)
+type t
+
+(** Test functions for special values to avoid calling [classify] *)
+val is_nan : t -> bool
+val is_infinity : t -> bool
+val is_neg_infinity : t -> bool
+
+val to_string : t -> string
+val of_string : string -> t
+
+val compile : t -> string
+
+val of_float : float -> t
+
+(** Return [true] for "-", [false] for "+". *)
+val sign : t -> bool
+
+val opp : t -> t
+val abs : t -> t
+
+type float_comparison = FEq | FLt | FGt | FNotComparable
+
+val eq : t -> t -> bool
+
+val lt : t -> t -> bool
+
+val le : t -> t -> bool
+
+(** The IEEE 754 float comparison.
+ * NotComparable is returned if there is a NaN in the arguments *)
+val compare : t -> t -> float_comparison
+[@@ocaml.inline always]
+
+type float_class =
+  | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+val classify : t -> float_class
+[@@ocaml.inline always]
+
+val mul : t -> t -> t
+
+val add : t -> t -> t
+
+val sub : t -> t -> t
+
+val div : t -> t -> t
+
+val sqrt : t -> t
+
+(** Link with integers *)
+val of_int63 : Uint63.t -> t
+[@@ocaml.inline always]
+
+val normfr_mantissa : t -> Uint63.t
+[@@ocaml.inline always]
+
+(** Shifted exponent extraction *)
+val eshift : int
+
+val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+[@@ocaml.inline always]
+
+val ldshiftexp : t -> Uint63.t -> t
+[@@ocaml.inline always]
+
+val next_up : t -> t
+
+val next_down : t -> t
+
+(** Return true if two floats are equal.
+ * All NaN values are considered equal. *)
+val equal : t -> t -> bool
+[@@ocaml.inline always]
+
+val hash : t -> int
+
+(** Total order relation over float values. Behaves like [Pervasives.compare].*)
+val total_compare : t -> t -> int
+
+val is_float64 : Obj.t -> bool
+[@@ocaml.inline always]
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index a8a4ffce9c..82bb2b584d 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -137,6 +137,26 @@ let opcodes =
     "CHECKTAIL0INT63";
     "ISINT";
     "AREINT2";
+    "CHECKOPPFLOAT";
+    "CHECKABSFLOAT";
+    "CHECKEQFLOAT";
+    "CHECKLTFLOAT";
+    "LTFLOAT";
+    "CHECKLEFLOAT";
+    "LEFLOAT";
+    "CHECKCOMPAREFLOAT";
+    "CHECKCLASSIFYFLOAT";
+    "CHECKADDFLOAT";
+    "CHECKSUBFLOAT";
+    "CHECKMULFLOAT";
+    "CHECKDIVFLOAT";
+    "CHECKSQRTFLOAT";
+    "CHECKFLOATOFINT63";
+    "CHECKFLOATNORMFRMANTISSA";
+    "CHECKFRSHIFTEXP";
+    "CHECKLDSHIFTEXP";
+    "CHECKNEXTUPFLOAT";
+    "CHECKNEXTDOWNFLOAT";
     "STOP"
   |]
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cd969ea457..320bc6a1cd 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -812,7 +812,7 @@ let rec subterm_specif renv stack t =
        | Not_subterm -> Not_subterm)
 
     | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
-      | Construct _ | CoFix _ | Int _ -> Not_subterm
+      | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm
 
 
       (* Other terms are not subterms *)
@@ -1057,7 +1057,7 @@ let check_one_fix renv recpos trees def =
 		    check_rec_call renv stack (Term.applist(c,l))
             end
 
-        | Sort _ | Int _ ->
+        | Sort _ | Int _ | Float _ ->
           assert (List.is_empty l)
 
         (* l is not checked because it is considered as the meta's context *)
@@ -1254,7 +1254,7 @@ let check_one_cofix env nbfix def deftype =
         | Evar _ ->
 	    List.iter (check_rec_call env alreadygrd n tree vlra) args
         | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
-          | Ind _ | Fix _ | Proj _ | Int _ ->
+          | Ind _ | Fix _ | Proj _ | Int _ | Float _ ->
            raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 3b8c2cd788..550c81ed82 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -102,6 +102,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     infer_vect infos variances (Array.map (mk_clos e) args)
   | FRel _ -> infer_stack infos variances stk
   | FInt _ -> infer_stack infos variances stk
+  | FFloat _ -> infer_stack infos variances stk
   | FFlex fl ->
     let variances = infer_table_key variances fl in
     infer_stack infos variances stk
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 20e742d7f8..2b83c2d868 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,6 +1,7 @@
 Names
 TransparentState
 Uint63
+Float64
 CPrimitives
 Univ
 UGraph
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1a5455cf3a..63dc49ba57 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -258,16 +258,19 @@ type primitive =
   | Mk_var of Id.t
   | Mk_proj
   | Is_int
+  | Is_float
   | Cast_accu
   | Upd_cofix
   | Force_cofix
   | Mk_uint
+  | Mk_float
   | Mk_int
   | Mk_bool
   | Val_to_int
   | Mk_meta
   | Mk_evar
   | MLand
+  | MLnot
   | MLle
   | MLlt
   | MLinteq
@@ -349,6 +352,9 @@ let primitive_hash = function
   | Mk_proj -> 36
   | MLarrayget -> 37
   | Mk_empty_instance -> 38
+  | Mk_float -> 39
+  | Is_float -> 40
+  | MLnot -> 41
 
 type mllambda =
   | MLlocal        of lname 
@@ -365,6 +371,7 @@ type mllambda =
                    (* prefix, inductive name, tag, arguments *)
   | MLint          of int
   | MLuint         of Uint63.t
+  | MLfloat        of Float64.t
   | MLsetref       of string * mllambda
   | MLsequence     of mllambda * mllambda
   | MLarray        of mllambda array
@@ -436,6 +443,8 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       Int.equal i1 i2
   | MLuint i1, MLuint i2 ->
       Uint63.equal i1 i2
+  | MLfloat f1, MLfloat f2 ->
+      Float64.equal f1 f2
   | MLsetref (id1, ml1), MLsetref (id2, ml2) ->
       String.equal id1 id2 &&
       eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
@@ -450,7 +459,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
     eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
   | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ |
     MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ |
-    MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false
+    MLfloat _ | MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false
 
 and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
   let eq_def (_,args1,ml1) (_,args2,ml2) =
@@ -535,6 +544,8 @@ let rec hash_mllambda gn n env t =
       combinesmall 15 (hash_mllambda_array gn n env 1 arr)
   | MLisaccu (s, ind, c) ->
       combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c)))
+  | MLfloat f ->
+      combinesmall 17 (Float64.hash f)
 
 and hash_mllambda_letrec gn n env init defs =
   let hash_def (_,args,ml) =
@@ -568,7 +579,7 @@ let fv_lam l =
     match l with
     | MLlocal l ->
 	if LNset.mem l bind then fv else LNset.add l fv
-    | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ -> fv
+    | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ | MLfloat _ -> fv
     | MLlam (ln,body) ->
 	let bind = Array.fold_right LNset.add ln bind in
 	aux body bind fv
@@ -757,7 +768,7 @@ type env =
       env_named : (Id.t * mllambda) list ref;
       env_univ : lname option}
 
-let empty_env univ () =
+let empty_env univ =
   { env_rel = [];
     env_bound = 0;
     env_urel = ref [];
@@ -958,25 +969,29 @@ type prim_aux =
   | PAprim of string * pconstant * CPrimitives.t * prim_aux array
   | PAml of mllambda
 
-let add_check cond args =
-  let aux cond a = 
+let add_check cond targs args =
+  let aux cond t a =
     match a with
     | PAml(MLint _) -> cond
     | PAml ml ->
        (* FIXME: use explicit equality function *)
-       if List.mem ml cond then cond else ml::cond 
+       if List.mem (t, ml) cond then cond else (t, ml)::cond
     | _ -> cond
   in
-  Array.fold_left aux cond args
+  Array.fold_left2 aux cond targs args
 
 let extract_prim ml_of l =
   let decl = ref [] in
   let cond = ref [] in
+  let type_args p =
+    let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
+    Array.of_list (aux (CPrimitives.types p)) in
   let rec aux l =
     match l with
     | Lprim(prefix,kn,p,args) ->
+      let targs = type_args p in
       let args = Array.map aux args in
-      cond := add_check !cond args;
+      cond := add_check !cond targs args;
       PAprim(prefix,kn,p,args)
     | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l)
     | _ ->
@@ -1010,15 +1025,35 @@ let compile_prim decl cond paux =
   let compile_cond cond paux =
     match cond with
     | [] -> opt_prim_aux paux
-    | [c1] ->
+    | [CPrimitives.(PITT_type PT_int63), c1] ->
       MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux)
-    | c1::cond ->
-      let cond =
-        List.fold_left
-          (fun ml c -> app_prim MLland [| ml; cast_to_int c|])
-          (app_prim MLland [| cast_to_int c1; MLint 0 |]) cond in
-      let cond = app_prim MLmagic [|cond|] in
-      MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in
+    | _ ->
+      let ci, cf =
+        let is_int =
+          function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in
+        List.partition is_int cond in
+      let condi =
+        let cond =
+          List.fold_left
+            (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|])
+            (MLint 0) ci in
+        app_prim MLmagic [|cond|] in
+      let condf = match cf with
+        | [] -> MLint 0
+        | [_, c1] -> app_prim Is_float [|c1|]
+        | (_, c1) :: condf ->
+           List.fold_left
+             (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|])
+             (app_prim Is_float [|c1|]) condf in
+      match ci, cf with
+      | [], [] -> opt_prim_aux paux
+      | _ :: _, [] ->
+         MLif(condi, naive_prim_aux paux, opt_prim_aux paux)
+      | [], _ :: _ ->
+         MLif(condf, opt_prim_aux paux, naive_prim_aux paux)
+      | _ :: _, _ :: _ ->
+         let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in
+         MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in
 
   let add_decl decl body =
     List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in
@@ -1095,14 +1130,14 @@ let ml_of_instance instance u =
          (* Remark: if we do not want to compile the predicate we 
             should a least compute the fv, then store the lambda representation
             of the predicate (not the mllambda) *)
-      let env_p = empty_env env.env_univ () in
+      let env_p = empty_env env.env_univ in
       let pn = fresh_gpred l in
       let mlp = ml_of_lam env_p l p in
       let mlp = generalize_fv env_p mlp in
       let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in
       let pn = push_global_let pn mlp in
       (* Compilation of the case *)
-      let env_c = empty_env env.env_univ () in
+      let env_c = empty_env env.env_univ in
       let a_uid = fresh_lname Anonymous in
       let la_uid = MLlocal a_uid in
       (* compilation of branches *)
@@ -1158,7 +1193,7 @@ let ml_of_instance instance u =
 	   start
       *)
       (* Compilation of type *)
-      let env_t = empty_env env.env_univ () in
+      let env_t = empty_env env.env_univ in
       let ml_t = Array.map (ml_of_lam env_t l) tt in
       let params_t = fv_params env_t in
       let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1167,7 +1202,7 @@ let ml_of_instance instance u =
       let mk_type = MLapp(MLglobal gft, args_t) in
       (* Compilation of norm_i *)
       let ndef = Array.length ids in
-      let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
+      let lf,env_n = push_rels (empty_env env.env_univ) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
       let mk_let _envi (id,def) t = MLlet (id,def,t) in
@@ -1224,7 +1259,7 @@ let ml_of_instance instance u =
       MLletrec(Array.mapi mkrec lf, lf_args.(start))
   | Lcofix (start, (ids, tt, tb)) -> 
       (* Compilation of type *)
-      let env_t = empty_env env.env_univ () in
+      let env_t = empty_env env.env_univ in
       let ml_t = Array.map (ml_of_lam env_t l) tt in
       let params_t = fv_params env_t in
       let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1233,7 +1268,7 @@ let ml_of_instance instance u =
       let mk_type = MLapp(MLglobal gft, args_t) in
       (* Compilation of norm_i *) 
       let ndef = Array.length ids in
-      let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
+      let lf,env_n = push_rels (empty_env env.env_univ) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
       let ml_of_fix i body =
@@ -1297,6 +1332,7 @@ let ml_of_instance instance u =
      let args = Array.map (ml_of_lam env l) args in
      MLconstruct(prefix,cn,tag,args)
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
+  | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1314,7 +1350,7 @@ let ml_of_instance instance u =
   | Lforce -> MLglobal (Ginternal "Lazy.force")
 
 let mllambda_of_lambda univ auxdefs l t =
-  let env = empty_env univ () in
+  let env = empty_env univ in
   global_stack := auxdefs;
   let ml = ml_of_lam env l t in
   let fv_rel = !(env.env_urel) in
@@ -1347,7 +1383,7 @@ let subst s l =
     let rec aux l =
       match l with
       | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-      | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
+      | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
       | MLlam(params,body) -> MLlam(params, aux body)
       | MLletrec(defs,body) ->
 	let arec (f,params,body) = (f,params,aux body) in
@@ -1417,7 +1453,7 @@ let optimize gdef l =
   let rec optimize s l =
     match l with
     | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-    | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
+    | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
     | MLlam(params,body) -> 
 	MLlam(params, optimize s body)
     | MLletrec(decls,body) ->
@@ -1623,6 +1659,7 @@ let pp_mllam fmt l =
           (string_of_construct prefix ~constant:false ind tag) pp_cargs args
     | MLint i -> pp_int fmt i
     | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
+    | MLfloat f -> Format.fprintf fmt "(%s)" (Float64.compile f)
     | MLsetref (s, body) ->
 	Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
     | MLsequence(l1,l2) ->
@@ -1739,16 +1776,19 @@ let pp_mllam fmt l =
         Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id)
     | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_int -> Format.fprintf fmt "is_int"
+    | Is_float -> Format.fprintf fmt "is_float"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
     | Mk_uint -> Format.fprintf fmt "mk_uint"
+    | Mk_float -> Format.fprintf fmt "mk_float"
     | Mk_int -> Format.fprintf fmt "mk_int"
     | Mk_bool -> Format.fprintf fmt "mk_bool"
     | Val_to_int -> Format.fprintf fmt "val_to_int"
     | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
     | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
     | MLand -> Format.fprintf fmt "(&&)"
+    | MLnot -> Format.fprintf fmt "not"
     | MLle -> Format.fprintf fmt "(<=)"
     | MLlt -> Format.fprintf fmt "(<)"
     | MLinteq -> Format.fprintf fmt "(==)"
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index dd010e5cad..ef610ce7e9 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -35,6 +35,9 @@ let rec conv_val env pb lvl v1 v2 cu =
 	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vint64 i1, Vint64 i2 ->
       if Int64.equal i1 i2 then cu else raise NotConvertible
+    | Vfloat64 f1, Vfloat64 f2 ->
+        if Float64.(equal (of_float f1) (of_float f2)) then cu
+        else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -48,7 +51,7 @@ let rec conv_val env pb lvl v1 v2 cu =
 	    aux lvl max b1 b2 (i+1) cu
 	in
 	aux lvl (n1-1) b1 b2 0 cu
-    | Vaccu _, _ | Vconst _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible
+    | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible
 
 and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 70b3beb2dc..7a4e62cdfe 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -44,6 +44,7 @@ type lambda =
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
   | Lind          of prefix * pinductive
@@ -123,7 +124,7 @@ let get_const_prefix env c =
 let map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
-  | Llazy | Lforce | Lmeta _ | Lint _ -> lam
+  | Llazy | Lforce | Lmeta _ | Lint _ | Lfloat _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -331,7 +332,7 @@ and reduce_lapp substf lids body substa largs =
 
 let is_value lc =
   match lc with
-  | Lval _ | Lint _ | Luint _ -> true
+  | Lval _ | Lint _ | Luint _ | Lfloat _ -> true
   | _ -> false
 
 let get_value lc =
@@ -339,6 +340,7 @@ let get_value lc =
   | Lval v -> v
   | Lint tag -> Nativevalues.mk_int tag
   | Luint i -> Nativevalues.mk_uint i
+  | Lfloat f -> Nativevalues.mk_float f
   | _ -> raise Not_found
 
 let make_args start _end =
@@ -364,7 +366,12 @@ let makeblock env ind tag nparams arity args =
   if Int.equal arity 0 then Lint tag
   else
   if Array.for_all is_value args then
-    let args = Array.map get_value args in
+    let dummy_val = Obj.magic 0 in
+    let args =
+      (* Don't simplify this to Array.map, cf. the related comment in
+         function eval_to_patch, file kernel/csymtable.ml *)
+      let a = Array.make (Array.length args) dummy_val in
+      Array.iteri (fun i v -> a.(i) <- get_value v) args; a in
     Lval (Nativevalues.mk_block tag args)
   else
     let prefix = get_mind_prefix env (fst ind) in
@@ -580,6 +587,8 @@ let rec lambda_of_constr cache env sigma c =
 
   | Int i -> Luint i
 
+  | Float f -> Lfloat f
+
 and lambda_of_app cache env sigma f args =
   match kind f with
   | Const (_kn,_u as c) ->
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index f17339f84d..1d7bf5343a 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -38,6 +38,7 @@ type lambda =
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
   | Lind          of prefix * pinductive
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index f788832d5b..e4a8344eaf 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -225,6 +225,9 @@ let mk_bool (b : bool) = (Obj.magic (not b) : t)
 let mk_uint (x : Uint63.t) = (Obj.magic x : t)
 [@@ocaml.inline always]
 
+let mk_float (x : Float64.t) = (Obj.magic x : t)
+[@@ocaml.inline always]
+
 type block
 
 let block_size (b:block) =
@@ -240,16 +243,19 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 let kind_of_value (v:t) =
   let o = Obj.repr v in
   if Obj.is_int o then Vconst (Obj.magic v)
+  else if Obj.tag o == Obj.double_tag then Vfloat64 (Obj.magic v)
   else
     let tag = Obj.tag o in
     if Int.equal tag accumulate_tag then
       Vaccu (Obj.magic v)
     else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+    else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
     else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
       else
         (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); 
@@ -261,6 +267,7 @@ let kind_of_value (v:t) =
 let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag
+[@@ocaml.inline always]
 
 let val_to_int (x:t) = (Obj.magic x : int)
 [@@ocaml.inline always]
@@ -508,6 +515,177 @@ let print x =
   flush stderr;
   x
 
+(** Support for machine floating point values *)
+
+external is_float : t -> bool = "coq_is_double"
+[@@noalloc]
+
+let to_float (x:t) = (Obj.magic x : Float64.t)
+[@@ocaml.inline always]
+
+let no_check_fopp x =
+  mk_float (Float64.opp (to_float x))
+[@@ocaml.inline always]
+
+let fopp accu x =
+  if is_float x then no_check_fopp x
+  else accu x
+
+let no_check_fabs x =
+  mk_float (Float64.abs (to_float x))
+[@@ocaml.inline always]
+
+let fabs accu x =
+  if is_float x then no_check_fabs x
+  else accu x
+
+let no_check_feq x y =
+  mk_bool (Float64.eq (to_float x) (to_float y))
+
+let feq accu x y =
+  if is_float x && is_float y then no_check_feq x y
+  else accu x y
+
+let no_check_flt x y =
+  mk_bool (Float64.lt (to_float x) (to_float y))
+
+let flt accu x y =
+  if is_float x && is_float y then no_check_flt x y
+  else accu x y
+
+let no_check_fle x y =
+  mk_bool (Float64.le (to_float x) (to_float y))
+
+let fle accu x y =
+  if is_float x && is_float y then no_check_fle x y
+  else accu x y
+
+type coq_fcmp =
+  | CFcmpAccu of t
+  | CFcmpEq
+  | CFcmpLt
+  | CFcmpGt
+  | CFcmpNotComparable
+
+let no_check_fcompare x y =
+  let c = Float64.compare (to_float x) (to_float y) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fcompare accu x y =
+  if is_float x && is_float y then no_check_fcompare x y
+  else accu x y
+
+type coq_fclass =
+  | CFclassAccu of t
+  | CFclassPNormal
+  | CFclassNNormal
+  | CFclassPSubn
+  | CFclassNSubn
+  | CFclassPZero
+  | CFclassNZero
+  | CFclassPInf
+  | CFclassNInf
+  | CFclassNaN
+
+let no_check_fclassify x =
+  let c = Float64.classify (to_float x) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fclassify accu x =
+  if is_float x then no_check_fclassify x
+  else accu x
+
+let no_check_fadd x y =
+  mk_float (Float64.add (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fadd accu x y =
+  if is_float x && is_float y then no_check_fadd x y
+  else accu x y
+
+let no_check_fsub x y =
+  mk_float (Float64.sub (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fsub accu x y =
+  if is_float x && is_float y then no_check_fsub x y
+  else accu x y
+
+let no_check_fmul x y =
+  mk_float (Float64.mul (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fmul accu x y =
+  if is_float x && is_float y then no_check_fmul x y
+  else accu x y
+
+let no_check_fdiv x y =
+  mk_float (Float64.div (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fdiv accu x y =
+  if is_float x && is_float y then no_check_fdiv x y
+  else accu x y
+
+let no_check_fsqrt x =
+  mk_float (Float64.sqrt (to_float x))
+[@@ocaml.inline always]
+
+let fsqrt accu x =
+  if is_float x then no_check_fsqrt x
+  else accu x
+
+let no_check_float_of_int x =
+  mk_float (Float64.of_int63 (to_uint x))
+[@@ocaml.inline always]
+
+let float_of_int accu x =
+  if is_int x then no_check_float_of_int x
+  else accu x
+
+let no_check_normfr_mantissa x =
+  mk_uint (Float64.normfr_mantissa (to_float x))
+[@@ocaml.inline always]
+
+let normfr_mantissa accu x =
+  if is_float x then no_check_normfr_mantissa x
+  else accu x
+
+let no_check_frshiftexp x =
+  let f, e = Float64.frshiftexp (to_float x) in
+  (Obj.magic (PPair(mk_float f, mk_uint e)):t)
+[@@ocaml.inline always]
+
+let frshiftexp accu x =
+  if is_float x then no_check_frshiftexp x
+  else accu x
+
+let no_check_ldshiftexp x e =
+  mk_float (Float64.ldshiftexp (to_float x) (to_uint e))
+[@@ocaml.inline always]
+
+let ldshiftexp accu x e =
+  if is_float x && is_int e then no_check_ldshiftexp x e
+  else accu x e
+
+let no_check_next_up x =
+  mk_float (Float64.next_up (to_float x))
+[@@ocaml.inline always]
+
+let next_up accu x =
+  if is_float x then no_check_next_up x
+  else accu x
+
+let no_check_next_down x =
+  mk_float (Float64.next_down (to_float x))
+[@@ocaml.inline always]
+
+let next_down accu x =
+  if is_float x then no_check_next_down x
+  else accu x
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b54f437e73..815ef3e98e 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -102,6 +102,9 @@ val mk_int : int -> t
 val mk_uint : Uint63.t -> t
 [@@ocaml.inline always]
 
+val mk_float : Float64.t -> t
+[@@ocaml.inline always]
+
 val napply : t -> t array -> t
 (* Functions over accumulators *)
 
@@ -130,6 +133,7 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 val kind_of_value : t -> kind_of_value
@@ -140,7 +144,9 @@ val str_decode : string -> 'a
 (** Support for machine integers *)
 
 val val_to_int : t -> int
+
 val is_int : t -> bool
+[@@ocaml.inline always]
 
 (* function with check *)
 val head0 : t -> t -> t
@@ -247,3 +253,82 @@ val no_check_le      : t -> t -> t
 [@@ocaml.inline always]
 
 val no_check_compare : t -> t -> t
+
+(** Support for machine floating point values *)
+
+val is_float : t -> bool
+[@@ocaml.inline always]
+
+val fopp : t -> t -> t
+val fabs : t -> t -> t
+val feq : t -> t -> t -> t
+val flt : t -> t -> t -> t
+val fle : t -> t -> t -> t
+val fcompare : t -> t -> t -> t
+val fclassify : t -> t -> t
+val fadd : t -> t -> t -> t
+val fsub : t -> t -> t -> t
+val fmul : t -> t -> t -> t
+val fdiv : t -> t -> t -> t
+val fsqrt : t -> t -> t
+val float_of_int : t -> t -> t
+val normfr_mantissa : t -> t -> t
+val frshiftexp : t -> t -> t
+val ldshiftexp : t -> t -> t -> t
+val next_up : t -> t -> t
+val next_down : t -> t -> t
+
+(* Function without check *)
+val no_check_fopp : t -> t
+[@@ocaml.inline always]
+
+val no_check_fabs : t -> t
+[@@ocaml.inline always]
+
+val no_check_feq : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_flt : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fle : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fcompare : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fclassify : t -> t
+[@@ocaml.inline always]
+
+val no_check_fadd : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsub : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fmul : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fdiv : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsqrt : t -> t
+[@@ocaml.inline always]
+
+val no_check_float_of_int : t -> t
+[@@ocaml.inline always]
+
+val no_check_normfr_mantissa : t -> t
+[@@ocaml.inline always]
+
+val no_check_frshiftexp : t -> t
+[@@ocaml.inline always]
+
+val no_check_ldshiftexp : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_next_up : t -> t
+[@@ocaml.inline always]
+
+val no_check_next_down : t -> t
+[@@ocaml.inline always]
diff --git a/kernel/primred.ml b/kernel/primred.ml
index d6d0a6143a..c475828cb3 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -14,6 +14,13 @@ let add_retroknowledge env action =
       | None -> { retro with retro_int63 = Some c }
       | Some c' -> assert (Constant.equal c c'); retro in
     set_retroknowledge env retro
+  | Register_type(PT_float64,c) ->
+    let retro = env.retroknowledge in
+    let retro =
+      match retro.retro_float64 with
+      | None -> { retro with retro_float64 = Some c }
+      | Some c' -> assert (Constant.equal c c'); retro in
+    set_retroknowledge env retro
   | Register_ind(pit,ind) ->
     let retro = env.retroknowledge in
     let retro =
@@ -42,6 +49,21 @@ let add_retroknowledge env action =
           | None -> ((ind,1), (ind,2), (ind,3))
           | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
         { retro with retro_cmp = Some r }
+      | PIT_f_cmp ->
+        let r =
+          match retro.retro_f_cmp with
+          | None -> ((ind,1), (ind,2), (ind,3), (ind,4))
+          | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
+        { retro with retro_f_cmp = Some r }
+      | PIT_f_class ->
+        let r =
+          match retro.retro_f_class with
+          | None -> ((ind,1), (ind,2), (ind,3), (ind,4),
+                     (ind,5), (ind,6), (ind,7), (ind,8),
+                     (ind,9))
+          | Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
+             assert (eq_ind ind ind'); t in
+        { retro with retro_f_class = Some r }
     in
     set_retroknowledge env retro
 
@@ -50,6 +72,17 @@ let get_int_type env =
   | Some c -> c
   | None -> anomaly Pp.(str"Reduction of primitive: int63 not registered")
 
+let get_float_type env =
+  match env.retroknowledge.retro_float64 with
+  | Some c -> c
+  | None -> anomaly Pp.(str"Reduction of primitive: float64 not registered")
+
+let get_cmp_type env =
+  match env.retroknowledge.retro_cmp with
+  | Some (((mindcmp,_),_),_,_) ->
+     Constant.make (MutInd.user mindcmp) (MutInd.canonical mindcmp)
+  | None -> anomaly Pp.(str"Reduction of primitive: comparison not registered")
+
 let get_bool_constructors env =
   match env.retroknowledge.retro_bool with
   | Some r -> r
@@ -70,6 +103,16 @@ let get_cmp_constructors env =
   | Some r -> r
   | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
 
+let get_f_cmp_constructors env =
+  match env.retroknowledge.retro_f_cmp with
+  | Some r -> r
+  | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
+
+let get_f_class_constructors env =
+  match env.retroknowledge.retro_f_class with
+  | Some r -> r
+  | None -> anomaly Pp.(str"Reduction of primitive: fclass not registered")
+
 exception NativeDestKO
 
 module type RedNativeEntries =
@@ -80,14 +123,29 @@ module type RedNativeEntries =
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
+    val get_float : evd -> elem -> Float64.t
     val mkInt : env -> Uint63.t -> elem
+    val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
     val mkCarry : env -> bool -> elem -> elem (* true if carry *)
     val mkIntPair : env -> elem -> elem -> elem
+    val mkFloatIntPair : env -> elem -> elem -> elem
     val mkLt : env -> elem
     val mkEq : env -> elem
     val mkGt : env -> elem
-
+    val mkFLt : env -> elem
+    val mkFEq : env -> elem
+    val mkFGt : env -> elem
+    val mkFNotComparable : env -> elem
+    val mkPNormal : env -> elem
+    val mkNNormal : env -> elem
+    val mkPSubn : env -> elem
+    val mkNSubn : env -> elem
+    val mkPZero : env -> elem
+    val mkNZero : env -> elem
+    val mkPInf : env -> elem
+    val mkNInf : env -> elem
+    val mkNaN : env -> elem
   end
 
 module type RedNative =
@@ -116,6 +174,12 @@ struct
   let get_int3 evd args =
     get_int evd args 0, get_int evd args 1, get_int evd args 2
 
+  let get_float evd args i = E.get_float evd (E.get args i)
+
+  let get_float1 evd args = get_float evd args 0
+
+  let get_float2 evd args = get_float evd args 0, get_float evd args 1
+
   let red_prim_aux env evd op args =
     let open CPrimitives in
     match op with
@@ -193,6 +257,64 @@ struct
         | 0 -> E.mkEq env
         | _ -> E.mkGt env
       end
+    | Float64opp ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
+    | Float64abs ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
+    | Float64eq ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.eq i1 i2)
+    | Float64lt ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.lt i1 i2)
+    | Float64le ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.le i1 i2)
+    | Float64compare ->
+      let f1, f2 = get_float2 evd args in
+      (match Float64.compare f1 f2 with
+      | Float64.FEq -> E.mkFEq env
+      | Float64.FLt -> E.mkFLt env
+      | Float64.FGt -> E.mkFGt env
+      | Float64.FNotComparable -> E.mkFNotComparable env)
+    | Float64classify ->
+      let f = get_float1 evd args in
+      (match Float64.classify f with
+      | Float64.PNormal -> E.mkPNormal env
+      | Float64.NNormal -> E.mkNNormal env
+      | Float64.PSubn -> E.mkPSubn env
+      | Float64.NSubn -> E.mkNSubn env
+      | Float64.PZero -> E.mkPZero env
+      | Float64.NZero -> E.mkNZero env
+      | Float64.PInf -> E.mkPInf env
+      | Float64.NInf -> E.mkNInf env
+      | Float64.NaN -> E.mkNaN env)
+    | Float64add ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
+    | Float64sub ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.sub f1 f2)
+    | Float64mul ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.mul f1 f2)
+    | Float64div ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.div f1 f2)
+    | Float64sqrt ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.sqrt f)
+    | Float64ofInt63 ->
+      let i = get_int1 evd args in E.mkFloat env (Float64.of_int63 i)
+    | Float64normfr_mantissa ->
+      let f = get_float1 evd args in E.mkInt env (Float64.normfr_mantissa f)
+    | Float64frshiftexp ->
+      let f = get_float1 evd args in
+      let (m,e) = Float64.frshiftexp f in
+      E.mkFloatIntPair env (E.mkFloat env m) (E.mkInt env e)
+    | Float64ldshiftexp ->
+      let f = get_float evd args 0 in
+      let e = get_int evd args 1 in
+      E.mkFloat env (Float64.ldshiftexp f e)
+    | Float64next_up ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.next_up f)
+    | Float64next_down ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.next_down f)
 
   let red_prim env evd p args =
     try
diff --git a/kernel/primred.mli b/kernel/primred.mli
index f5998982d7..bbe564d8e7 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -5,10 +5,17 @@ open Environ
 val add_retroknowledge : env -> Retroknowledge.action -> env
 
 val get_int_type : env -> Constant.t
+val get_float_type : env -> Constant.t
+val get_cmp_type : env -> Constant.t
 val get_bool_constructors : env -> constructor * constructor
 val get_carry_constructors : env -> constructor * constructor
 val get_pair_constructor : env -> constructor
 val get_cmp_constructors : env -> constructor * constructor * constructor
+val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
+val get_f_class_constructors :
+  env -> constructor * constructor * constructor * constructor
+         * constructor * constructor * constructor * constructor
+         * constructor
 
 exception NativeDestKO (* Should be raised by get_* functions on failure *)
 
@@ -20,13 +27,29 @@ module type RedNativeEntries =
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
+    val get_float : evd -> elem -> Float64.t
     val mkInt : env -> Uint63.t -> elem
+    val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
     val mkCarry : env -> bool -> elem -> elem (* true if carry *)
     val mkIntPair : env -> elem -> elem -> elem
+    val mkFloatIntPair : env -> elem -> elem -> elem
     val mkLt : env -> elem
     val mkEq : env -> elem
     val mkGt : env -> elem
+    val mkFLt : env -> elem
+    val mkFEq : env -> elem
+    val mkFGt : env -> elem
+    val mkFNotComparable : env -> elem
+    val mkPNormal : env -> elem
+    val mkNNormal : env -> elem
+    val mkPSubn : env -> elem
+    val mkNSubn : env -> elem
+    val mkPZero : env -> elem
+    val mkNZero : env -> elem
+    val mkPInf : env -> elem
+    val mkNInf : env -> elem
+    val mkNaN : env -> elem
   end
 
 module type RedNative =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 327cb2efeb..0cc7692fcf 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -138,10 +138,10 @@ let nf_betaiota env t =
 let whd_betaiotazeta env x =
   match kind x with
   | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|Int _) -> x
+       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> x
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ -> x
+      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
@@ -152,10 +152,10 @@ let whd_betaiotazeta env x =
 let whd_all env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|Int _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | Int _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos all env) (create_tab ()) (inject t)
@@ -166,10 +166,10 @@ let whd_all env t =
 let whd_allnolet env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
         | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
@@ -627,13 +627,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
        if Uint63.equal i1 i2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        else raise NotConvertible
 
+    | FFloat f1, FFloat f2 ->
+        if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
-        | FProd _ | FEvar _ | FInt _), _ -> raise NotConvertible
+        | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 873c6af93d..479fe02295 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -18,23 +18,37 @@ open Names
 
 type retroknowledge = {
     retro_int63 : Constant.t option;
+    retro_float64 : Constant.t option;
     retro_bool : (constructor * constructor) option; (* true, false *)
     retro_carry : (constructor * constructor) option; (* C0, C1 *)
     retro_pair : constructor option;
     retro_cmp : (constructor * constructor * constructor) option;
                     (* Eq, Lt, Gt *)
-    retro_refl : constructor option;
+    retro_f_cmp : (constructor * constructor * constructor * constructor)
+                  option;
+                  (* FEq, FLt, FGt, FNotComparable *)
+    retro_f_class : (constructor * constructor * constructor * constructor
+                     * constructor * constructor * constructor * constructor
+                     * constructor)
+                      option;
+                    (* PNormal, NNormal, PSubn, NSubn,
+                       PZero, NZero, PInf, NInf,
+                       NaN *)
+    retro_refl : constructor option
 }
 
 let empty = {
     retro_int63 = None;
+    retro_float64 = None;
     retro_bool = None;
     retro_carry = None;
     retro_pair = None;
     retro_cmp = None;
+    retro_f_cmp = None;
+    retro_f_class = None;
     retro_refl = None;
 }
 
 type action =
-  | Register_ind of CPrimitives.prim_ind * inductive
-  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
+  | Register_type : CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 2a7b390951..2df8a00465 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -12,16 +12,27 @@ open Names
 
 type retroknowledge = {
     retro_int63 : Constant.t option;
+    retro_float64 : Constant.t option;
     retro_bool : (constructor * constructor) option; (* true, false *)
     retro_carry : (constructor * constructor) option; (* C0, C1 *)
     retro_pair : constructor option;
     retro_cmp : (constructor * constructor * constructor) option;
                     (* Eq, Lt, Gt *)
-    retro_refl : constructor option;
+    retro_f_cmp : (constructor * constructor * constructor * constructor)
+                  option;
+                    (* FEq, FLt, FGt, FNotComparable *)
+    retro_f_class : (constructor * constructor * constructor * constructor
+                     * constructor * constructor * constructor * constructor
+                     * constructor)
+                      option;
+                    (* PNormal, NNormal, PSubn, NSubn,
+                       PZero, NZero, PInf, NInf,
+                       NaN *)
+    retro_refl : constructor option
 }
 
 val empty : retroknowledge
 
 type action =
-  | Register_ind of CPrimitives.prim_ind * inductive
-  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
+  | Register_type : CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index f398e6a5da..5c15257511 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -60,7 +60,7 @@ let rec relevance_of_fterm env extra lft f =
       | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
       | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
       | FFlex key -> relevance_of_flex env extra lft key
-      | FInt _ -> Sorts.Relevant
+      | FInt _ | FFloat _ -> Sorts.Relevant
       | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
       | FConstruct (c,_) -> relevance_of_constructor env c
       | FApp (f, _) -> relevance_of_fterm env extra lft f
@@ -105,7 +105,7 @@ and relevance_of_term_extra env extra lft subs c =
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
-  | Int _ -> Sorts.Relevant
+  | Int _ | Float _ -> Sorts.Relevant
 
   | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e846b17aa0..d3cffd1546 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1327,7 +1327,7 @@ let register_inline kn senv =
   let cb = {cb with const_inline_code = true} in
   let env = add_constant kn cb env in { senv with env}
 
-let check_register_ind ind r env =
+let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
   let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in
   let check_if b msg =
     if not b then
@@ -1403,6 +1403,36 @@ let check_register_ind ind r env =
     check_type_cte 1;
     check_name 2 "Gt";
     check_type_cte 2
+  | CPrimitives.PIT_f_cmp ->
+    check_nconstr 4;
+    check_name 0 "FEq";
+    check_type_cte 0;
+    check_name 1 "FLt";
+    check_type_cte 1;
+    check_name 2 "FGt";
+    check_type_cte 2;
+    check_name 3 "FNotComparable";
+    check_type_cte 3
+  | CPrimitives.PIT_f_class ->
+    check_nconstr 9;
+    check_name 0 "PNormal";
+    check_type_cte 0;
+    check_name 1 "NNormal";
+    check_type_cte 1;
+    check_name 2 "PSubn";
+    check_type_cte 2;
+    check_name 3 "NSubn";
+    check_type_cte 3;
+    check_name 4 "PZero";
+    check_type_cte 4;
+    check_name 5 "NZero";
+    check_type_cte 5;
+    check_name 6 "PInf";
+    check_type_cte 6;
+    check_name 7 "NInf";
+    check_type_cte 7;
+    check_name 8 "NaN";
+    check_type_cte 8
 
 let register_inductive ind prim senv =
   check_register_ind ind prim senv.env;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b2f6668577..ae6993b0e2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -226,7 +226,7 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t
 (** {6 Retroknowledge / Native compiler } *)
 
 val register_inline : Constant.t -> safe_transformer0
-val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0
+val register_inductive : inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
 
 val set_strategy :
   Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0
diff --git a/kernel/term.ml b/kernel/term.ml
index 38c0d043cf..7343507838 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -383,4 +383,4 @@ let kind_of_type t = match kind t with
   | (Rel _ | Meta _ | Var _ | Evar _ | Const _ 
   | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
     -> AtomicType (t,[||])
-  | (Lambda _ | Construct _ | Int _) -> failwith "Not a type"
+  | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b87384d228..1cc40a6707 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -215,14 +215,22 @@ let type_of_apply env func funt argsv argstv =
 (* Type of primitive constructs *)
 let type_of_prim_type _env = function
   | CPrimitives.PT_int63 -> Constr.mkSet
+  | CPrimitives.PT_float64 -> Constr.mkSet
 
 let type_of_int env =
   match env.retroknowledge.Retroknowledge.retro_int63 with
   | Some c -> mkConst c
   | None -> CErrors.user_err Pp.(str"The type int must be registered before this construction can be typechecked.")
 
+let type_of_float env =
+  match env.retroknowledge.Retroknowledge.retro_float64 with
+  | Some c -> mkConst c
+  | None -> raise
+        (Invalid_argument "Typeops.type_of_float: float64 not_defined")
+
 let type_of_prim env t =
-  let int_ty = type_of_int env in
+  let int_ty () = type_of_int env in
+  let float_ty () = type_of_float env in
   let bool_ty () =
     match env.retroknowledge.Retroknowledge.retro_bool with
     | Some ((ind,_),_) -> Constr.mkInd ind
@@ -233,6 +241,16 @@ let type_of_prim env t =
     | Some ((ind,_),_,_) -> Constr.mkInd ind
     | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
   in
+  let f_compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_cmp with
+    | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
+  in
+  let f_class_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_class with
+    | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
+  in
   let pair_ty fst_ty snd_ty =
     match env.retroknowledge.Retroknowledge.retro_pair with
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
@@ -243,39 +261,27 @@ let type_of_prim env t =
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
     | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
   in
-  let rec nary_int63_op arity ty =
-    if Int.equal arity 0 then ty
-      else Constr.mkProd(Context.nameR (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty)
-  in
-  let return_ty =
-    let open CPrimitives in
-    match t with
-    | Int63head0
-    | Int63tail0
-    | Int63add
-    | Int63sub
-    | Int63mul
-    | Int63div
-    | Int63mod
-    | Int63lsr
-    | Int63lsl
-    | Int63land
-    | Int63lor
-    | Int63lxor
-    | Int63addMulDiv -> int_ty
-    | Int63eq
-    | Int63lt
-    | Int63le -> bool_ty ()
-    | Int63mulc
-    | Int63div21
-    | Int63diveucl -> pair_ty int_ty int_ty
-    | Int63addc
-    | Int63subc
-    | Int63addCarryC
-    | Int63subCarryC -> carry_ty int_ty
-    | Int63compare -> compare_ty ()
-  in
-  nary_int63_op (CPrimitives.arity t) return_ty
+  let open CPrimitives in
+  let tr_prim_type = function
+    | PT_int63 -> int_ty ()
+    | PT_float64 -> float_ty () in
+  let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with
+    | PIT_bool, () -> bool_ty ()
+    | PIT_carry, t -> carry_ty (tr_prim_type t)
+    | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
+    | PIT_cmp, () -> compare_ty ()
+    | PIT_f_cmp, () -> f_compare_ty ()
+    | PIT_f_class, () -> f_class_ty () in
+  let tr_type = function
+    | PITT_ind (i, a) -> tr_ind i a
+    | PITT_type t -> tr_prim_type t in
+  let rec nary_op = function
+    | [] -> assert false
+    | [ret_ty] -> tr_type ret_ty
+    | arg_ty :: r ->
+       let arg_ty = tr_type arg_ty in
+       Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in
+  nary_op (types t)
 
 let type_of_prim_or_type env = let open CPrimitives in
   function
@@ -285,6 +291,9 @@ let type_of_prim_or_type env = let open CPrimitives in
 let judge_of_int env i =
   make_judge (Constr.mkInt i) (type_of_int env)
 
+let judge_of_float env f =
+  make_judge (Constr.mkFloat f) (type_of_float env)
+
 (* Type of product *)
 
 let sort_of_product env domsort rangsort =
@@ -583,6 +592,7 @@ let rec execute env cstr =
 
     (* Primitive types *)
     | Int _ -> cstr, type_of_int env
+    | Float _ -> cstr, type_of_float env
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index c71a0e0ca4..ae816fe26e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -120,6 +120,9 @@ val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit
 val type_of_int : env -> types
 val judge_of_int : env -> Uint63.t -> unsafe_judgment
 
+val type_of_float : env -> types
+val judge_of_float : env -> Float64.t -> unsafe_judgment
+
 val type_of_prim_type : env -> CPrimitives.prim_type -> types
 val type_of_prim : env -> CPrimitives.t -> types
 
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index d22ba3468f..e0bf44da35 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -19,7 +19,14 @@ val to_int2 : t -> int * int (* msb, lsb *)
 val of_int64 : Int64.t -> t
 (*
 val of_uint : int -> t
-*)
+ *)
+(** [int_min n m] returns the minimum of [n] and [m],
+    [m] must be in [0, 2^30-1]. *)
+val to_int_min : t -> int -> int
+
+      (* conversion to float *)
+val of_float : float -> t
+val to_float : t -> float
 
 val hash : t -> int
 
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index b8eccd19fb..e38389ca13 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -26,6 +26,13 @@ let mask63 i = Int64.logand i maxuint63
 let of_int i = Int64.of_int i
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
 let of_int64 i = i
+
+let to_int_min n m =
+  if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
+
+let of_float f = mask63 (Int64.of_float f)
+let to_float = Int64.to_float
+
 let hash i =
   let (h,l) = to_int2 i in
   (*Hashset.combine h l*)
@@ -213,4 +220,8 @@ let () =
   Callback.register "uint63 one" one;
   Callback.register "uint63 sub" sub;
   Callback.register "uint63 subcarry" subcarry;
-  Callback.register "uint63 tail0" tail0
+  Callback.register "uint63 tail0" tail0;
+  Callback.register "uint63 of_float" of_float;
+  Callback.register "uint63 to_float" to_float;
+  Callback.register "uint63 of_int" of_int;
+  Callback.register "uint63 to_int_min" to_int_min
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..85b44528a7 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,6 +27,12 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let of_float = int_of_float
+
+external to_float : int -> (float [@unboxed])
+  = "coq_uint63_to_float_byte" "coq_uint63_to_float"
+[@@noalloc]
+
 let hash i = i
 [@@ocaml.inline always]
 
@@ -96,6 +102,10 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+let to_int_min n m =
+  if lt n m then n else m
+[@@ocaml.inline always]
+
     (* division of two numbers by one *)
 (* precondition: xh < y *)
 (* outputs: q, r s.t. x = q * y + r, r < y *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 414c443c4e..5d36ad54a2 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -73,6 +73,9 @@ and conv_whd env pb k whd1 whd2 cu =
       else raise NotConvertible
   | Vint64 i1, Vint64 i2 ->
     if Int64.equal i1 i2 then cu else raise NotConvertible
+  | Vfloat64 f1, Vfloat64 f2 ->
+    if Float64.(equal (of_float f1) (of_float f2)) then cu
+    else raise NotConvertible
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
@@ -80,7 +83,7 @@ and conv_whd env pb k whd1 whd2 cu =
       conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _ | Vint64 _, _
-  | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+  | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
 
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 319a26d824..5f08720f77 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -169,7 +169,8 @@ let rec apply_stack a stk v =
 let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
-  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ -> assert false
+  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ ->
+     assert false
   | Vfun f -> reduce_fun k f
   | Vfix(f, None) -> 
       push_ra stop;
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index c8f5020d71..5acdd964b1 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -57,6 +57,7 @@ type structured_constant =
   | Const_univ_level of Univ.Level.t
   | Const_val of structured_values
   | Const_uint of Uint63.t
+  | Const_float of Float64.t
 
 type reloc_table = (tag * int) array
 
@@ -75,6 +76,8 @@ let rec eq_structured_values v1 v2 =
        Int.equal (Obj.size o1) (Obj.size o2)
     then if Int.equal t1 Obj.custom_tag
       then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64)
+    else if Int.equal t1 Obj.double_tag
+      then Float64.(equal (of_float (Obj.magic v1)) (of_float (Obj.magic v2)))
     else begin
       assert (t1 <= Obj.last_non_constant_constructor_tag &&
               t2 <= Obj.last_non_constant_constructor_tag);
@@ -105,6 +108,8 @@ let eq_structured_constant c1 c2 = match c1, c2 with
 | Const_val _, _ -> false
 | Const_uint i1, Const_uint i2 -> Uint63.equal i1 i2
 | Const_uint _, _ -> false
+| Const_float f1, Const_float f2 -> Float64.equal f1 f2
+| Const_float _, _ -> false
 
 let hash_structured_constant c =
   let open Hashset.Combine in
@@ -115,6 +120,7 @@ let hash_structured_constant c =
   | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l)
   | Const_val v -> combinesmall 5 (hash_structured_values v)
   | Const_uint i -> combinesmall 6 (Uint63.hash i)
+  | Const_float f -> combinesmall 7 (Float64.hash f)
 
 let eq_annot_switch asw1 asw2 =
   let eq_ci ci1 ci2 =
@@ -149,6 +155,7 @@ let pp_struct_const = function
   | Const_univ_level l -> Univ.Level.pr l
   | Const_val _ -> Pp.str "(value)"
   | Const_uint i -> Pp.str (Uint63.to_string i)
+  | Const_float f -> Pp.str (Float64.to_string f)
 
 (* Abstract data *)
 type vprod
@@ -284,6 +291,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vint64 of int64
+  | Vfloat64 of float
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t
 
@@ -315,6 +323,7 @@ let uni_lvl_val (v : values) : Univ.Level.t =
         | Vconstr_const _i -> str "Vconstr_const"
         | Vconstr_block _b -> str "Vconstr_block"
         | Vint64 _ -> str "Vint64"
+        | Vfloat64 _ -> str "Vfloat64"
         | Vatom_stk (_a,_stk) -> str "Vatom_stk"
         | Vuniv_level _ -> assert false
       in
@@ -374,6 +383,8 @@ let rec whd_accu a stk =
       end
   | i when Int.equal i Obj.custom_tag ->
     Vint64 (Obj.magic i)
+  | i when Int.equal i Obj.double_tag ->
+    Vfloat64 (Obj.magic i)
   | tg ->
     CErrors.anomaly
       Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
@@ -403,6 +414,7 @@ let whd_val : values -> whd =
            | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
            | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
         else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+        else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
         else
            Vconstr_block(Obj.obj o)
 
@@ -426,6 +438,7 @@ let obj_of_str_const str =
   | Const_univ_level l -> Obj.repr (Vuniv_level l)
   | Const_val v -> Obj.repr v
   | Const_uint i -> Obj.repr i
+  | Const_float f -> Obj.repr f
 
 let val_of_block tag (args : structured_values array) =
   let nargs = Array.length args in
@@ -675,6 +688,7 @@ and pr_whd w =
   | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
   | Vconstr_block _b -> str "Vconstr_block"
   | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str
+  | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")"
   | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
   | Vuniv_level _ -> assert false)
 and pr_stack stk =
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d289e7db9a..9c24006ff0 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -45,6 +45,7 @@ type structured_constant =
   | Const_univ_level of Univ.Level.t
   | Const_val of structured_values
   | Const_uint of Uint63.t
+  | Const_float of Float64.t
 
 val pp_struct_const : structured_constant -> Pp.t
 
@@ -127,6 +128,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vint64 of int64
+  | Vfloat64 of float
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t