From c823ad32033904fc47cda9a9ae9f3fa3116edc6f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 May 2023 17:34:08 +0200
Subject: Make progress on extracting the HOL4 files

---
 compiler/Translate.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 709b54a4..1107a123 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -851,7 +851,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   (* Close the module *)
   (match !Config.backend with
   | FStar | Lean -> ()
-  | HOL4 -> Printf.fprintf out "val _ = export_theory \"%s\"\n" module_name
+  | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
   | Coq -> Printf.fprintf out "End %s .\n" module_name);
 
   (* Some logging *)
-- 
cgit v1.2.3