diff options
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0781a811..7d8e84c4 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -961,10 +961,18 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) ctx def.inputs_lvs in (* Print the return type *) - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - extract_ty ctx fmt false (Collections.List.to_cons_nil def.signature.outputs); + let _ = + F.pp_print_space fmt (); + (* Open a box for the return type *) + F.pp_open_hovbox fmt 0; + (* Print the return type *) + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + extract_ty ctx fmt false + (Collections.List.to_cons_nil def.signature.outputs); + (* Close the box for the return type *) + F.pp_close_box fmt () + in (* Print the "=" *) F.pp_print_space fmt (); F.pp_print_string fmt "="; |