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