From ee797b755311d397744bbe008ffb4be5180530e4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Feb 2022 16:32:11 +0100
Subject: Make minor improvements

---
 src/ExtractToFStar.ml | 3 ++-
 src/Translate.ml      | 4 ++++
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'src')

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 *)
-- 
cgit v1.2.3