5 files changed, 31 insertions, 6 deletions
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 942cbe8916..a0b25afc37 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -45,6 +45,7 @@ Ltac2 Type kind := [
 | CoFix (int, ident option binder_annot array, constr array, constr array)
 | Proj (projection, constr)
 | Uint63 (uint63)
+| Float (float)
 ].
 
 Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 6eed261554..65f0a362b1 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -17,6 +17,7 @@ Ltac2 Type string.
 Ltac2 Type char.
 Ltac2 Type ident.
 Ltac2 Type uint63.
+Ltac2 Type float.
 
 (** Constr-specific built-in types *)
 Ltac2 Type meta.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 6ab80575dd..55cd7f7692 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -450,7 +450,8 @@ let () = define1 "constr_kind" constr begin fun c ->
     |]
   | Int n ->
     v_blk 17 [|Value.of_uint63 n|]
-  | Float _ -> assert false
+  | Float f ->
+    v_blk 18 [|Value.of_float f|]
   end
 end
 
@@ -531,6 +532,9 @@ let () = define1 "constr_make" valexpr begin fun knd ->
   | (17, [|n|]) ->
     let n = Value.to_uint63 n in
     EConstr.mkInt n
+  | (18, [|f|]) ->
+    let f = Value.to_float f in
+    EConstr.mkFloat f
   | _ -> assert false
   in
   return (Value.of_constr c)
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index 7c9613f31b..9ae17bf9bc 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -33,6 +33,8 @@ type valexpr =
   (** Arbitrary data *)
 | ValUint63 of Uint63.t
   (** Primitive integers *)
+| ValFloat of Float64.t
+  (** Primitive floats *)
 
 and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure
 
@@ -50,21 +52,21 @@ type t = valexpr
 
 let is_int = function
 | ValInt _ -> true
-| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false
+| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ | ValFloat _ -> false
 
 let tag v = match v with
 | ValBlk (n, _) -> n
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ | ValFloat _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let field v n = match v with
 | ValBlk (_, v) -> v.(n)
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ | ValFloat _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let set_field v n w = match v with
 | ValBlk (_, v) -> v.(n) <- w
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ | ValFloat _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let make_block tag v = ValBlk (tag, v)
@@ -196,7 +198,7 @@ let of_closure cls = ValCls cls
 
 let to_closure = function
 | ValCls cls -> cls
-| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ | ValFloat _ -> assert false
 
 let closure = {
   r_of = of_closure;
@@ -333,6 +335,17 @@ let uint63 = {
   r_id = false;
 }
 
+let of_float f = ValFloat f
+let to_float = function
+| ValFloat f -> f
+| _ -> assert false
+
+let float = {
+  r_of = of_float;
+  r_to = to_float;
+  r_id = false;
+}
+
 let of_constant c = of_ext val_constant c
 let to_constant c = to_ext val_constant c
 let constant = repr_ext val_constant
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index d3c9596e8f..ee13f00568 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -32,6 +32,8 @@ type valexpr =
   (** Arbitrary data *)
 | ValUint63 of Uint63.t
   (** Primitive integers *)
+| ValFloat of Float64.t
+  (** Primitive floats *)
 
 type 'a arity
 
@@ -151,6 +153,10 @@ val of_uint63 : Uint63.t -> valexpr
 val to_uint63 : valexpr -> Uint63.t
 val uint63 : Uint63.t repr
 
+val of_float : Float64.t -> valexpr
+val to_float : valexpr -> Float64.t
+val float : Float64.t repr
+
 type ('a, 'b) fun1
 
 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic