aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 0d29a239..831f92f6 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -392,7 +392,7 @@ let rec convertExpr env e =
| C.EConst(C.CFloat(f, k, _)) ->
if k = C.FLongDouble then
unsupported "'long double' floating-point literal";
- Eval(Vfloat(f), ty)
+ Eval(Vfloat(coqfloat_of_camlfloat f), ty)
| C.EConst(C.CStr s) ->
let ty = typeStringLiteral s in
Evalof(Evar(name_for_string_literal env s, ty), ty)