summaryrefslogtreecommitdiff
path: root/caml/Floataux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'caml/Floataux.ml')
-rw-r--r--caml/Floataux.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/caml/Floataux.ml b/caml/Floataux.ml
index 0226de2..6b3b825 100644
--- a/caml/Floataux.ml
+++ b/caml/Floataux.ml
@@ -19,6 +19,9 @@ let singleoffloat f =
let intoffloat f =
coqint_of_camlint (Int32.of_float f)
+let intuoffloat f =
+ coqint_of_camlint (Int64.to_int32 (Int64.of_float f))
+
let floatofint i =
Int32.to_float (camlint_of_coqint i)