diff options
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index cfbca6e6..57b1b560 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -18,6 +18,7 @@ open Datatypes open BinPos open BinInt +open Floats (* Integers *) @@ -116,6 +117,13 @@ let camlstring_of_coqstring (s: char list) = | c :: s -> r.[pos] <- c; fill (pos + 1) s in fill 0 s +(* Floats *) + +let coqfloat_of_camlfloat f = + Float.double_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)) + (* Timing facility *) (* |