summaryrefslogtreecommitdiff
path: root/cparser
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-11 16:28:40 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-11 16:28:40 +0000
commit45fc4cc348d2b8c4cc151a5e3ce3483f21a6ef78 (patch)
tree51384cafb70c58f7b380d77a2871d4fbe550c08f /cparser
parenta5b2f37fd69b903dabd44f1f7f19894e62e497d0 (diff)
Suppress int64_unsigned_to_float, now unused.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Ceval.ml2
-rw-r--r--cparser/uint64.c5
2 files changed, 0 insertions, 7 deletions
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 5770e27..d38054a 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -21,8 +21,6 @@ open Machine
(* Extra arith on int64 *)
-external int64_unsigned_to_float: int64 -> float
- = "cparser_int64_unsigned_to_float"
external int64_unsigned_div: int64 -> int64 -> int64
= "cparser_int64_unsigned_div"
external int64_unsigned_mod: int64 -> int64 -> int64
diff --git a/cparser/uint64.c b/cparser/uint64.c
index 5396617..1528887 100644
--- a/cparser/uint64.c
+++ b/cparser/uint64.c
@@ -16,11 +16,6 @@
#include <caml/mlvalues.h>
#include <caml/alloc.h>
-value cparser_int64_unsigned_to_float(value v)
-{
- return caml_copy_double((double)((uint64) Int64_val(v)));
-}
-
value cparser_int64_unsigned_div(value v1, value v2)
{
return caml_copy_int64((uint64) Int64_val(v1) / (uint64) Int64_val(v2));