diff options
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 9441d71..4e0ee7f 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -191,6 +191,8 @@ let print_typed_value p v ty = fprintf p "%ld" (camlint_of_coqint n) | Vfloat f, _ -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Vsingle f, _ -> + fprintf p "%Ff" (camlfloat_of_coqfloat32 f) | Vlong n, Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> |