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

18 files changed, 214 insertions, 27 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43b94aed3d..c78f791a5a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -220,14 +220,26 @@ module VNativeEntries =
           | _ -> raise Primred.NativeDestKO)
       | _ -> raise Primred.NativeDestKO
 
+    let get_float () e =
+      match e with
+      | VAL(_, cf) ->
+        (match kind cf with
+        | Float f -> f
+        | _ -> raise Primred.NativeDestKO)
+      | _ -> raise Primred.NativeDestKO
+
     let mkInt env i = VAL(0, mkInt i)
 
+    let mkFloat env f = VAL(0, mkFloat f)
+
     let mkBool env b =
       let (ct,cf) = get_bool_constructors env in
       CONSTR(Univ.in_punivs (if b then ct else cf), [||])
 
     let int_ty env = VAL(0, mkConst @@ get_int_type env)
 
+    let float_ty env = VAL(0, mkConst @@ get_float_type env)
+
     let mkCarry env b e =
       let (c0,c1) = get_carry_constructors env in
       CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|])
@@ -237,6 +249,12 @@ module VNativeEntries =
       let c = get_pair_constructor env in
       CONSTR(Univ.in_punivs c, [|int_ty;int_ty;e1;e2|])
 
+    let mkFloatIntPair env f i =
+      let float_ty = float_ty env in
+      let int_ty = int_ty env in
+      let c = get_pair_constructor env in
+      CONSTR(Univ.in_punivs c, [|float_ty;int_ty;f;i|])
+
     let mkLt env =
       let (_eq,lt,_gt) = get_cmp_constructors env in
       CONSTR(Univ.in_punivs lt, [||])
@@ -249,6 +267,66 @@ module VNativeEntries =
       let (_eq,_lt,gt) = get_cmp_constructors env in
       CONSTR(Univ.in_punivs gt, [||])
 
+    let mkFLt env =
+      let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs lt, [||])
+
+    let mkFEq env =
+      let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs eq, [||])
+
+    let mkFGt env =
+      let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs gt, [||])
+
+    let mkFNotComparable env =
+      let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs nc, [||])
+
+    let mkPNormal env =
+      let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pNormal, [||])
+
+    let mkNNormal env =
+      let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nNormal, [||])
+
+    let mkPSubn env =
+      let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pSubn, [||])
+
+    let mkNSubn env =
+      let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nSubn, [||])
+
+    let mkPZero env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pZero, [||])
+
+    let mkNZero env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nZero, [||])
+
+    let mkPInf env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pInf, [||])
+
+    let mkNInf env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nInf, [||])
+
+    let mkNaN env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nan, [||])
   end
 
 module VredNative = RedNative(VNativeEntries)
@@ -381,7 +459,7 @@ let rec norm_head info env t stack =
   | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
-  | (Sort _ | Meta _ | Ind _ | Int _) -> (VAL(0, t), stack)
+  | (Sort _ | Meta _ | Ind _ | Int _ | Float _) -> (VAL(0, t), stack)
   | Prod _ -> (CBN(t,env), stack)
 
 and norm_head_ref k info env stack normt t =
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index e85c888b2e..d1cc21d82f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -406,9 +406,10 @@ let matches_core env sigma allow_bound_rels
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          Array.fold_left2 (sorec ctx env) subst args1 args2
       | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
+      | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
          | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
-         | PFix _ | PCoFix _| PEvar _ | PInt _), _ -> raise PatternMatchingFailure
+         | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _), _ -> raise PatternMatchingFailure
 
   in
   sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
@@ -526,7 +527,7 @@ let sub_match ?(closed=true) env sigma pat c =
       aux env term mk_ctx next
     with Retyping.RetypeError _ -> next ()
     end
-  | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ | Int _ ->
+  | Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ ->
     next ()
   in
   here next
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e8c83c7de9..5dd4772bcc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -834,6 +834,7 @@ and detype_r d flags avoid env sigma t =
     | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
+    | Float f -> GFloat f
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
@@ -1027,6 +1028,7 @@ let rec subst_glob_constr env subst = DAst.map (function
   | GVar _
   | GEvar _
   | GInt _
+  | GFloat _
   | GPatVar _ as raw -> raw
 
   | GApp (r,rl) as raw ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 288a349b8b..73d0c6f821 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -138,7 +138,7 @@ let flex_kind_of_term flags env evd c sk =
     | Evar ev ->
        if is_frozen flags ev then Rigid
        else Flexible ev
-    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid
+    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
@@ -220,7 +220,7 @@ let occur_rigidly flags env evd (evk,_) t =
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
-    | Meta _ | Fix _ | CoFix _ | Int _ -> Reducible
+    | Meta _ | Fix _ | CoFix _ | Int _ | Float _ -> Reducible
   in
     match aux t with
     | Rigid b -> b
@@ -899,7 +899,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              only if necessary) or the second argument is potentially
              usable as a canonical projection or canonical value *)
           let rec is_unnamed (hd, args) = match EConstr.kind i hd with
-            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _) ->
+            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _) ->
 	      Stack.not_purely_applicative args
             | (CoFix _|Meta _|Rel _)-> true
             | Evar _ -> Stack.not_purely_applicative args
@@ -1019,7 +1019,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	| Const _, Const _
 	| Ind _, Ind _ 
         | Construct _, Construct _
-        | Int _, Int _ ->
+        | Int _, Int _
+        | Float _, Float _ ->
           rigids env evd sk1 term1 sk2 term2
 
         | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *)
@@ -1064,7 +1065,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
 	  end
 
-        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _), _ ->
+        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Evar _ | Lambda _), _ ->
 	  UnifFailure (evd,NotSameHead)
         | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) ->
           UnifFailure (evd,NotSameHead)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 93f5923474..03bb633fa0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -156,9 +156,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
   | GInt i1, GInt i2 -> Uint63.equal i1 i2
+  | GFloat f1, GFloat f2 -> Float64.equal f1 f2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
      GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ |
-     GInt _), _ -> false
+     GInt _ | GFloat _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -219,7 +220,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
-  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) as x -> x
+  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) as x -> x
   )
 
 let map_glob_constr = map_glob_constr_left_to_right
@@ -251,7 +252,7 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
-  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc
   )
 let fold_return_type_with_binders f g v acc (na,tyopt) =
   Option.fold_left (f (Name.fold_right g na v)) acc tyopt
@@ -293,7 +294,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
     f v acc c
-  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc))
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc))
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 10e9d60fd5..44323441b6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -91,6 +91,7 @@ type 'a glob_constr_r =
   | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
   | GInt of Uint63.t
+  | GFloat of Float64.t
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
 and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 870df62500..7740628c21 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -79,7 +79,7 @@ and kind_of_head env t =
   | Proj (p,c) -> RigidHead RigidOther
 
   | Case (_,_,c,_) -> aux k [] c true
-  | Int _ -> ConstructorHead
+  | Int _ | Float _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
       try aux k [] (List.nth l n) true
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index f8eecd80d4..39a4a525ef 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -26,6 +26,7 @@ type key =
   | KCoFix
   | KRel
   | KInt
+  | KFloat
 
 module KeyOrdered = struct
   type t = key
@@ -42,6 +43,7 @@ module KeyOrdered = struct
     | KCoFix -> 6
     | KRel -> 7
     | KInt -> 8
+    | KFloat -> 9
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -135,6 +137,7 @@ let constr_key kind c =
       | Sort _ -> KSort
       | LetIn _ -> KLet
       | Int _ -> KInt
+      | Float _ -> KFloat
     in Some (aux c)
   with Not_found -> None
 
@@ -151,6 +154,7 @@ let pr_key pr_global = function
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
   | KInt -> str"Int"
+  | KFloat -> str"Float"
 
 let pr_keyset pr_global v =
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index e5aed300a2..0178d5c009 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -208,6 +208,7 @@ let rec nf_val env sigma v typ =
       mkLambda(name,dom,body)
   | Vconst n -> construct_of_constr_const env sigma n typ
   | Vint64 i -> i |> Uint63.of_int64 |> mkInt
+  | Vfloat64 f -> f |> Float64.of_float |> mkFloat
   | Vblock b ->
       let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
       let args = nf_bargs env sigma b ctyp in
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index e0beb383b5..2d7a152817 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -40,6 +40,7 @@ type constr_pattern =
   | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
   | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
   | PInt of Uint63.t
+  | PFloat of Float64.t
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ccc3b6e83c..0c4312dc77 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -62,9 +62,12 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
    Projection.equal p1 p2 && constr_pattern_eq t1 t2
 | PInt i1, PInt i2 ->
    Uint63.equal i1 i2
+| PFloat f1, PFloat f2 ->
+   Float64.equal f1 f2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
    | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
-   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _), _ -> false
+   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _
+   | PFloat _), _ -> false
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -92,7 +95,7 @@ let rec occur_meta_pattern = function
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _
-    | PInt _ -> false
+    | PInt _ | PFloat _ -> false
 
 let rec occurn_pattern n = function
   | PRel p -> Int.equal n p
@@ -113,7 +116,7 @@ let rec occurn_pattern n = function
       (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> Array.exists (occurn_pattern n) args
-  | PVar _ | PRef _ | PSort _ | PInt _ -> false
+  | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
   | PFix (_,(_,tl,bl)) ->
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
   | PCoFix (_,(_,tl,bl)) ->
@@ -136,7 +139,7 @@ let rec head_pattern_bound t =
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
+    | PCoFix _ | PInt _ | PFloat _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> GlobRef.ConstRef sp
@@ -213,7 +216,8 @@ let pattern_of_constr env sigma t =
        let env' = Array.fold_left2 push env lna tl in
        PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl,
                   Array.map (pattern_of_constr env') bl))
-    | Int i -> PInt i in
+    | Int i -> PInt i
+    | Float f -> PFloat f in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -235,7 +239,8 @@ let map_pattern_with_binders g f l = function
      let l' = Array.fold_left (fun l na -> g na l) l lna in
      PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _ as x) -> x
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _
+     | PFloat _ as x) -> x
 
 let error_instantiate_pattern id l =
   let is = match l with
@@ -290,7 +295,8 @@ let rec subst_pattern env sigma subst pat =
   | PVar _
   | PEvar _
   | PRel _
-  | PInt _ -> pat
+  | PInt _
+  | PFloat _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
       let c' = subst_pattern env sigma subst c in
@@ -495,6 +501,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PCoFix (n, (names, tl, cl))
 
   | GInt i -> PInt i
+  | GFloat f -> PFloat f
   | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4fed526cfc..2e1cb9ff08 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1026,6 +1026,13 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env :
             user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
+  | GFloat f ->
+      let resj =
+        try Typing.judge_of_float !!env f
+        with Invalid_argument _ ->
+          user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.")
+        in
+        inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
 and pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index df161b747a..2952466fbb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -848,9 +848,17 @@ struct
     | Int i -> i
     | _ -> raise Primred.NativeDestKO
 
+  let get_float evd e =
+    match EConstr.kind evd e with
+    | Float f -> f
+    | _ -> raise Primred.NativeDestKO
+
   let mkInt env i =
     mkInt i
 
+  let mkFloat env f =
+    mkFloat f
+
   let mkBool env b =
     let (ct,cf) = get_bool_constructors env in
     mkConstruct (if b then ct else cf)
@@ -865,6 +873,12 @@ struct
     let c = get_pair_constructor env in
     mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|])
 
+  let mkFloatIntPair env f i =
+    let float_ty = mkConst @@ get_float_type env in
+    let int_ty = mkConst @@ get_int_type env in
+    let c = get_pair_constructor env in
+    mkApp(mkConstruct c, [|float_ty;int_ty;f;i|])
+
   let mkLt env =
     let (_eq, lt, _gt) = get_cmp_constructors env in
     mkConstruct lt
@@ -877,6 +891,66 @@ struct
     let (_eq, _lt, gt) = get_cmp_constructors env in
     mkConstruct gt
 
+  let mkFLt env =
+    let (_eq, lt, _gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct lt
+
+  let mkFEq env =
+    let (eq, _lt, _gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct eq
+
+  let mkFGt env =
+    let (_eq, _lt, gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct gt
+
+  let mkFNotComparable env =
+    let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in
+    mkConstruct nc
+
+  let mkPNormal env =
+    let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pNormal
+
+  let mkNNormal env =
+    let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nNormal
+
+  let mkPSubn env =
+    let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pSubn
+
+  let mkNSubn env =
+    let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nSubn
+
+  let mkPZero env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pZero
+
+  let mkNZero env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nZero
+
+  let mkPInf env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pInf
+
+  let mkNInf env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nInf
+
+  let mkNaN env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+      get_f_class_constructors env in
+    mkConstruct nan
 end
 
 module CredNative = RedNative(CNativeEntries)
@@ -1135,7 +1209,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|_ -> fold ()
       else fold ()
 
-    | Int i ->
+    | Int _ | Float _ ->
       begin match Stack.strip_app stack with
        | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) ->
          let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
@@ -1238,7 +1312,7 @@ let local_whd_state_gen flags sigma =
       else s
 
     | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _  | Ind _ | Proj _
-      | Int _ -> s
+      | Int _ | Float _ -> s
 
   in
   whrec
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cc341afac3..966c8f6e12 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -146,6 +146,7 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
     | Int _ -> EConstr.of_constr (Typeops.type_of_int env)
+    | Float _ -> EConstr.of_constr (Typeops.type_of_float env)
 
   and sort_of env t =
     match EConstr.kind sigma t with
@@ -281,7 +282,7 @@ let relevance_of_term env sigma c =
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
       | Proj (p, _) -> Retypeops.relevance_of_projection env p
-      | Int _ -> Sorts.Relevant
+      | Int _ | Float _ -> Sorts.Relevant
 
       | Meta _ | Evar _ -> Sorts.Relevant
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2db5512ff4..1a145fe1b2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -319,6 +319,9 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) =
 let judge_of_int env v =
   Environ.on_judgment EConstr.of_constr (judge_of_int env v)
 
+let judge_of_float env v =
+  Environ.on_judgment EConstr.of_constr (judge_of_float env v)
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env sigma cstr =
@@ -430,6 +433,9 @@ let rec execute env sigma cstr =
     | Int i ->
         sigma, judge_of_int env i
 
+    | Float f ->
+        sigma, judge_of_float env f
+
 and execute_recdef env sigma (names,lar,vdef) =
   let sigma, larj = execute_array env sigma lar in
   let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 63fb0679f1..1b07b2bb78 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -57,3 +57,4 @@ val judge_of_product : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
 val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment
 val judge_of_int : Environ.env -> Uint63.t -> unsafe_judgment
+val judge_of_float : Environ.env -> Float64.t -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4d34139ec0..7147580b3d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -566,7 +566,7 @@ let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
   | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
-  | Construct _ | Int _ -> true
+  | Construct _ | Int _ | Float _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
     | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _)
@@ -661,7 +661,7 @@ let rec is_neutral env sigma ts t =
     | Evar _ | Meta _ -> true
     | Case (_, p, c, cl) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
-    | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ -> false
+    | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
     | Fix _ -> false (* This is an approximation *)
     | App _ -> assert false
@@ -1821,7 +1821,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 
           | Cast (_, _, _) (* Is this expected? *)
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
-            | Construct _ | Int _ -> user_err Pp.(str "Match_subterm")))
+            | Construct _ | Int _ | Float _ -> user_err Pp.(str "Match_subterm")))
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
@@ -1890,7 +1890,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
           | Cast (_, _, _)  -> fail "Match_subterm" (* Is this expected? *)
 
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
-            | Construct _ | Int _ -> fail "Match_subterm"))
+            | Construct _ | Int _ | Float _ -> fail "Match_subterm"))
 
   in
   let res = matchrec cl [] in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index da0a92f284..d15eb578c3 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -169,6 +169,7 @@ and nf_whd env sigma whd typ =
       let args = nf_bargs env sigma b ofs ctyp in
       mkApp(capp,args)
   | Vint64 i -> i |> Uint63.of_int64 |> mkInt
+  | Vfloat64 f -> f |> Float64.of_float |> mkFloat
   | Vatom_stk(Aid idkey, stk) ->
       constr_type_of_idkey env sigma idkey stk
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->