summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Translate.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index 47426c81..a5189606 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -340,6 +340,8 @@ let translate_module (filename : string) (config : C.partial_config)
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_string fmt "open Primitives";
+ 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;