summaryrefslogtreecommitdiff
path: root/lib/Camlcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Camlcoq.ml')
-rw-r--r--lib/Camlcoq.ml9
1 files changed, 7 insertions, 2 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 8d6fd24..dd89636 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -320,9 +320,14 @@ let coqstring_of_camlstring s =
(* Floats *)
let coqfloat_of_camlfloat f =
- Float.double_of_bits(coqint_of_camlint64(Int64.bits_of_float f))
+ Float.of_bits(coqint_of_camlint64(Int64.bits_of_float f))
let camlfloat_of_coqfloat f =
- Int64.float_of_bits(camlint64_of_coqint(Float.bits_of_double f))
+ Int64.float_of_bits(camlint64_of_coqint(Float.to_bits f))
+
+let coqfloat32_of_camlfloat f =
+ Float32.of_bits(coqint_of_camlint(Int32.bits_of_float f))
+let camlfloat_of_coqfloat32 f =
+ Int32.float_of_bits(camlint_of_coqint(Float32.to_bits f))
(* Int31 *)