Make minor improvements

2 files changed, 6 insertions, 1 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index c0dcea71..f4cc0d6c 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -386,6 +386,8 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def)
    * body translation: the updated ctx we return at the end of the function
    * only contains the registered type def and variant names *)
   let ctx_body, type_params = ctx_add_type_params def.type_params ctx in
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   F.pp_print_string fmt ("(** [" ^ Print.name_to_string def.name ^ "] *)");
   F.pp_print_space fmt ();
@@ -419,5 +421,4 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def)
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0;
   F.pp_print_break fmt 0 0
diff --git a/src/Translate.ml b/src/Translate.ml
index 2ddc4adc..874d852e 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -330,6 +330,10 @@ let translate_module (filename : string) (config : C.partial_config)
   Format.pp_print_break fmt 0 0;
   Format.pp_print_string fmt ("module " ^ module_name);
   Format.pp_print_break fmt 0 0;
+  Format.pp_print_string fmt "open FStar.Mul";
+  Format.pp_print_break fmt 0 0;
+  Format.pp_print_break fmt 0 0;
+  Format.pp_print_string fmt "#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\"";
   Format.pp_print_break fmt 0 0;
 
   (* Export the definition groups to the file, in the proper order *)