diff options
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index d86e137a..c9d6fced 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -18,7 +18,7 @@ open Format open Camlcoq open AST -open Ctypes +open! Ctypes open Cop open Clight @@ -221,6 +221,14 @@ let asttype p t = | AST.Tany32 -> "AST.Tany32" | AST.Tany64 -> "AST.Tany64") +let astrettype p = function + | AST.Tret t -> asttype p t + | AST.Tvoid -> fprintf p "AST.Tvoid" + | AST.Tint8signed -> fprintf p "AST.Tint8signed" + | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned" + | AST.Tint16signed -> fprintf p "AST.Tint16signed" + | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned" + let name_of_chunk = function | Mint8signed -> "Mint8signed" | Mint8unsigned -> "Mint8unsigned" @@ -236,7 +244,7 @@ let name_of_chunk = function let signatur p sg = fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]" (print_list asttype) sg.sig_args - (print_option asttype) sg.sig_res + astrettype sg.sig_res callconv sg.sig_cc let assertions = ref ([]: (string * typ list) list) |