diff options
Diffstat (limited to 'caml/Floataux.ml')
| -rw-r--r-- | caml/Floataux.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/caml/Floataux.ml b/caml/Floataux.ml index 0226de27..6b3b825f 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) |