From 380bb3bdb7858fb9fbf40a6f56001a79e70ba7f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Feb 2022 10:23:37 +0100
Subject: Remove the `open FStar.Mul` line from the generated files

---
 src/Translate.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Translate.ml b/src/Translate.ml
index 252be079..cca131e6 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -338,8 +338,6 @@ 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_string fmt "open Primitives";
   Format.pp_print_break fmt 0 0;
   Format.pp_print_break fmt 0 0;
-- 
cgit v1.2.3