summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-10 10:31:37 +0100
committerSon Ho2022-02-10 10:31:37 +0100
commit8e3be66093318a4a31419ae5018f9d413d756cd5 (patch)
tree44d70a429d3014a57844dfd1d78441f182c32654
parent2a4aa027a496c95533f7970ff791420380e55e1f (diff)
Make slight improvements to formatting
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml4
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";