diff options
Diffstat (limited to 'cfrontend/Ctypes.v')
| -rw-r--r-- | cfrontend/Ctypes.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bf483a0..8d00b95 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -530,6 +530,7 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist := Definition typ_of_type (t: type) : AST.typ := match t with + | Tfloat F32 _ => AST.Tsingle | Tfloat _ _ => AST.Tfloat | Tlong _ _ => AST.Tlong | _ => AST.Tint @@ -538,6 +539,7 @@ Definition typ_of_type (t: type) : AST.typ := Definition opttyp_of_type (t: type) : option AST.typ := match t with | Tvoid => None + | Tfloat F32 _ => Some AST.Tsingle | Tfloat _ _ => Some AST.Tfloat | Tlong _ _ => Some AST.Tlong | _ => Some AST.Tint |