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.

16 files changed, 113 insertions, 27 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43b94aed3d..520bcd6b41 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -220,14 +220,29 @@ 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 cmp_ty env = VAL(0, mkConst @@ get_cmp_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 +252,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 +270,15 @@ module VNativeEntries =
       let (_eq,_lt,gt) = get_cmp_constructors env in
       CONSTR(Univ.in_punivs gt, [||])
 
+    let mkSomeCmp env v =
+      let cmp_ty = cmp_ty env in
+      let (some,_none) = get_option_constructors env in
+      CONSTR(Univ.in_punivs some, [|cmp_ty;v|])
+
+    let mkNoneCmp env =
+      let cmp_ty = cmp_ty env in
+      let (_some,none) = get_option_constructors env in
+      CONSTR(Univ.in_punivs none, [|cmp_ty|])
   end
 
 module VredNative = RedNative(VNativeEntries)
@@ -381,7 +411,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/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..12419c04bc 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,15 @@ struct
     let (_eq, _lt, gt) = get_cmp_constructors env in
     mkConstruct gt
 
+  let mkSomeCmp env v =
+    let cmp_ty = mkConst @@ get_cmp_type env in
+    let (some, _none) = get_option_constructors env in
+    mkApp(mkConstruct some, [|cmp_ty;v|])
+
+  let mkNoneCmp env =
+    let cmp_ty = mkConst @@ get_cmp_type env in
+    let (_some, none) = get_option_constructors env in
+    mkApp(mkConstruct none, [|cmp_ty|])
 end
 
 module CredNative = RedNative(CNativeEntries)
@@ -1135,7 +1158,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 +1261,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