diff options
Diffstat (limited to 'common/PrintAST.ml')
| -rw-r--r-- | common/PrintAST.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/common/PrintAST.ml b/common/PrintAST.ml index c18b09d..9768447 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -16,7 +16,11 @@ open Printf open Camlcoq open AST -let name_of_type = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long" +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + | Tlong -> "long" + | Tsingle -> "single" let name_of_chunk = function | Mint8signed -> "int8signed" |