summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-10 10:08:50 +0100
committerSon Ho2022-02-10 10:08:50 +0100
commit2a4aa027a496c95533f7970ff791420380e55e1f (patch)
tree43da03b893a7d703e031fba01514481d9abcb705
parentdcff2372f056af24c176b90797c10412b8b5f893 (diff)
Improve slightly more the formatting
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml9
1 files changed, 6 insertions, 3 deletions
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 *)