diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 3 | ||||
| -rw-r--r-- | src/Translate.ml | 4 |
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 *) |