Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.

31 files changed, 477 insertions, 37 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 3fd613e905..5f0da5da65 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,23 @@ 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_option = ref false
+    let fSome = ref dummy
+    let fNone = ref dummy
+
+    let init_option retro =
+      match retro.Retroknowledge.retro_option with
+      | Some (cSome, cNone) ->
+        defined_option := true;
+        fSome := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cSome) };
+        fNone := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNone) }
+      | None -> defined_option := false
+
     let defined_refl = ref false
 
     let frefl = ref dummy
@@ -1044,10 +1078,12 @@ 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_option !current_retro;
       init_refl !current_retro
 
     let check_env env =
@@ -1057,6 +1093,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 +1113,18 @@ module FNativeEntries =
       check_env env;
       assert (!defined_cmp)
 
+    let check_option env =
+      check_env env;
+      assert (!defined_option)
+
     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 +1138,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 +1155,15 @@ module FNativeEntries =
       check_cmp env;
       !fGt
 
+    let mkSomeCmp env v =
+      check_cmp env;
+      check_option env;
+      { mark = mark Cstr KnownR; term = FApp(!fSome, [|!fcmp;v|]) }
+
+    let mkNoneCmp env =
+      check_cmp env;
+      check_option env;
+      { mark = mark Cstr KnownR; term = FApp(!fNone, [|!fcmp|]) }
   end
 
 module FredNative = RedNative(FNativeEntries)
@@ -1164,7 +1226,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 +1332,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 d433cdc1ba..3154ee8c75 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -33,6 +33,18 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64compare
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
 
 let equal (p1 : t) (p2 : t) =
   p1 == p2
@@ -62,6 +74,18 @@ let hash = function
   | Int63lt -> 22
   | Int63le -> 23
   | Int63compare -> 24
+  | Float64opp -> 25
+  | Float64abs -> 26
+  | Float64compare -> 27
+  | Float64add -> 28
+  | Float64sub -> 29
+  | Float64mul -> 30
+  | Float64div -> 31
+  | Float64sqrt -> 32
+  | Float64ofInt63 -> 33
+  | Float64normfr_mantissa -> 34
+  | Float64frshiftexp -> 35
+  | Float64ldshiftexp -> 36
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -89,15 +113,29 @@ let to_string = function
   | Int63lt -> "lt"
   | Int63le -> "le"
   | Int63compare -> "compare"
+  | Float64opp -> "fopp"
+  | Float64abs -> "fabs"
+  | Float64compare -> "fcompare"
+  | Float64add -> "fadd"
+  | Float64sub -> "fsub"
+  | Float64mul -> "fmul"
+  | Float64div -> "fdiv"
+  | Float64sqrt -> "fsqrt"
+  | Float64ofInt63 -> "float_of_int"
+  | Float64normfr_mantissa -> "normfr_mantissa"
+  | Float64frshiftexp -> "frshiftexp"
+  | Float64ldshiftexp -> "ldshiftexp"
 
 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_option : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
@@ -107,6 +145,7 @@ 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
@@ -122,6 +161,14 @@ let types =
   | 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 -> [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))]
+  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())]
+  | 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 *)
@@ -130,7 +177,7 @@ 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 arity t = List.length (types t) - 1
@@ -150,9 +197,11 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
+  | PIT_option -> "option"
 
 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 3c825a8018..f9424fb09d 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -33,6 +33,18 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64compare
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
 
 val equal : t -> t -> bool
 
@@ -55,12 +67,14 @@ val kind : t -> args_red
 
 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_option : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
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..181211d237 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -234,6 +234,7 @@ let check_prim_op = function
   | Int63lt        -> opCHECKLTINT63
   | Int63le        -> opCHECKLEINT63
   | Int63compare   -> opCHECKCOMPAREINT63
+  | _ -> 0 (* TODO: BERTHOLON add float64 operations *)
 
 let emit_instr env = function
   | Klabel lbl -> define_label env lbl
@@ -384,7 +385,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/float64.ml b/kernel/float64.ml
new file mode 100644
index 0000000000..e74fd2e9f1
--- /dev/null
+++ b/kernel/float64.ml
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   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
+
+(* OCaml give a sign to nan values which should not be displayed as all nan are
+ * considered equal *)
+let to_string f = if is_nan f then "nan" else string_of_float f
+let of_string = float_of_string
+
+let opp = ( ~-. )
+let abs = abs_float
+
+type float_comparison = Eq | Lt | Gt | NotComparable
+
+let compare x y =
+  if x < y then Lt
+  else
+  (
+    if x > y then Gt
+    else
+    (
+      if x = y then Eq
+      else NotComparable (* NaN case *)
+    )
+  )
+
+let mul = ( *. )
+let add = ( +. )
+let sub = ( -. )
+let div = ( /. )
+let sqrt = sqrt
+
+let of_int63 = Uint63.to_float
+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
+
+let eshift = 1022 + 52 (* minimum negative exponent + binary precision *)
+
+(* 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)
+
+let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift)
+
+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. *)
+
+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 Util.pervasives_compare (1. /. f1) (1. /. f2)
+  else Util.pervasives_compare f1 f2
diff --git a/kernel/float64.mli b/kernel/float64.mli
new file mode 100644
index 0000000000..fd84f9e61d
--- /dev/null
+++ b/kernel/float64.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*         *   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
+
+val is_nan : t -> bool
+
+val to_string : t -> string
+val of_string : string -> t
+
+val opp : t -> t
+val abs : t -> t
+
+type float_comparison = Eq | Lt | Gt | NotComparable
+
+(** The IEEE 754 float comparison.
+ * NotComparable is returned if there is a NaN in the arguments *)
+val compare : t -> t -> float_comparison
+
+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
+val normfr_mantissa : t -> Uint63.t
+
+(** Shifted exponent extraction *)
+val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+val ldshiftexp : t -> Uint63.t -> t
+
+(** Return true if two floats are equal.
+ * All NaN values are considered equal. *)
+val equal : t -> t -> bool
+
+val hash : t -> int
+
+(** Total order relation over float values. Behaves like [Pervasives.compare].*)
+val total_compare : t -> t -> int
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/nativelambda.ml b/kernel/nativelambda.ml
index 70b3beb2dc..301773143c 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -580,6 +580,8 @@ let rec lambda_of_constr cache env sigma c =
 
   | Int i -> Luint i
 
+  | Float _ -> assert false  (* native computed for primitive float not yet implemented *)
+
 and lambda_of_app cache env sigma f args =
   match kind f with
   | Const (_kn,_u as c) ->
diff --git a/kernel/primred.ml b/kernel/primred.ml
index d6d0a6143a..1b9badfca9 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,12 @@ 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_option ->
+        let r =
+          match retro.retro_option with
+          | None -> ((ind,1), (ind,2))
+          | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+        { retro with retro_option = Some r }
     in
     set_retroknowledge env retro
 
@@ -50,6 +63,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 +94,11 @@ let get_cmp_constructors env =
   | Some r -> r
   | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
 
+let get_option_constructors env =
+  match env.retroknowledge.retro_option with
+  | Some r -> r
+  | None -> anomaly Pp.(str"Reduction of primitive: option not registered")
+
 exception NativeDestKO
 
 module type RedNativeEntries =
@@ -80,14 +109,18 @@ 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 mkSomeCmp : env -> elem -> elem
+    val mkNoneCmp : env -> elem
   end
 
 module type RedNative =
@@ -116,6 +149,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 +232,39 @@ 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)
+    | Float64compare ->
+      let f1, f2 = get_float2 evd args in
+      (match Float64.compare f1 f2 with
+      | Float64.Eq -> E.mkSomeCmp env (E.mkEq env)
+      | Float64.Lt -> E.mkSomeCmp env (E.mkLt env)
+      | Float64.Gt -> E.mkSomeCmp env (E.mkGt env)
+      | Float64.NotComparable -> E.mkNoneCmp 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)
 
   let red_prim env evd p args =
     try
diff --git a/kernel/primred.mli b/kernel/primred.mli
index f5998982d7..b2c9ebc6ea 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -5,10 +5,13 @@ 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_option_constructors : env -> constructor * constructor
 
 exception NativeDestKO (* Should be raised by get_* functions on failure *)
 
@@ -20,13 +23,18 @@ 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 mkSomeCmp : env -> elem -> elem
+    val mkNoneCmp : 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 48a6ff4c96..a84353bdc6 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -18,20 +18,24 @@ 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_option : (constructor * constructor) option; (* Some, None *)
     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_option = None;
     retro_refl = None;
 }
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0eb3eaf940..0aca296d29 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -12,11 +12,13 @@ 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_option : (constructor * constructor) option; (* Some, None *)
     retro_refl : constructor option;
 }
 
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 52bd9a6ada..000f6125a6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1403,6 +1403,27 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
     check_type_cte 1;
     check_name 2 "Gt";
     check_type_cte 2
+  | CPrimitives.PIT_option ->
+    check_nconstr 2;
+    check_name 0 "Some";
+    let cSome = ob.mind_user_lc.(0) in
+    let s = Pp.str "the first option constructor (Some) has a wrong type" in
+    begin match Term.decompose_prod cSome with
+      | ([_,v;_,_V], codom) ->
+        check_if (is_Type _V) s;
+        check_if (Constr.equal v (mkRel 1)) s;
+        check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s
+      | _ -> check_if false s
+    end;
+    check_name 1 "None";
+    let cNone = ob.mind_user_lc.(1) in
+    let s = Pp.str "the second option constructor (None) has a wrong type" in
+    begin match Term.decompose_prod cNone with
+      | ([_,_V], codom) ->
+        check_if (is_Type _V) s;
+        check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s
+      | _ -> check_if false s
+    end
 
 let register_inductive ind prim senv =
   check_register_ind ind prim senv.env;
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 a967711a83..a9913772f2 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
@@ -238,6 +246,11 @@ let type_of_prim env t =
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
     | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
   in
+  let option_ty ty =
+    match env.retroknowledge.Retroknowledge.retro_option with
+    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
+    | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
+  in
   let carry_ty int_ty =
     match env.retroknowledge.Retroknowledge.retro_carry with
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -245,12 +258,14 @@ let type_of_prim env t =
   in
   let open CPrimitives in
   let tr_prim_type = function
-    | PT_int63 -> int_ty in
+    | 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 () in
+    | PIT_cmp, () -> compare_ty ()
+    | PIT_option, () -> option_ty (compare_ty ()) in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
@@ -270,6 +285,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 =
@@ -568,6 +586,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..c7d1e36451 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -21,6 +21,10 @@ val of_int64 : Int64.t -> t
 val of_uint : int -> t
 *)
 
+      (* conversion to float *)
+val of_float : float -> t
+val to_float : t -> float
+
 val hash : t -> int
 
      (* conversion to a string *)
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index b8eccd19fb..76d768e20a 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -26,6 +26,10 @@ 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 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*)
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..4c9377b628 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,6 +27,9 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let of_float = int_of_float
+let to_float i = Int64.to_float (to_uint64 i)
+
 let hash i = i
 [@@ocaml.inline always]
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index c8f5020d71..fe3c76c960 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
 
@@ -105,6 +106,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 +118,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 +153,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
@@ -426,6 +431,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
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d289e7db9a..1e40801be0 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