summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
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";