diff options
author | Son Ho | 2022-02-10 10:31:37 +0100 |
---|---|---|
committer | Son Ho | 2022-02-10 10:31:37 +0100 |
commit | 8e3be66093318a4a31419ae5018f9d413d756cd5 (patch) | |
tree | 44d70a429d3014a57844dfd1d78441f182c32654 | |
parent | 2a4aa027a496c95533f7970ff791420380e55e1f (diff) |
Make slight improvements to formatting
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index ccce4e1a..cca2b22c 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1088,11 +1088,11 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) * TODO: figure out a cleaner way *) let _ = F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + 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 (); (* `Tot` *) if has_decreases_clause then ( F.pp_print_string fmt "Tot"; |