From 2a4aa027a496c95533f7970ff791420380e55e1f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 10 Feb 2022 10:08:50 +0100
Subject: Improve slightly more the formatting

---
 src/ExtractToFStar.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index def63db7..ccce4e1a 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1033,13 +1033,16 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_string fmt ":";
   F.pp_print_space fmt ();
   F.pp_print_string fmt "nat";
-  (* Print the body *)
+  (* Print the "=" *)
   F.pp_print_space fmt ();
   F.pp_print_string fmt "=";
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "admit ()";
   (* Close the box for "let FUN_NAME (PARAMS) =" *)
   F.pp_close_box fmt ();
+  (* Add a space before the "admit" and increment the indentation if we need
+   * to break line *)
+  F.pp_print_break fmt 1 ctx.indent_incr;
+  (* Print the "admit ()" *)
+  F.pp_print_string fmt "admit ()";
   (* Close the box for the whole definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-- 
cgit v1.2.3