Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 2 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 8d6fd243..dd896367 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 *)