summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Translate.ml')
-rw-r--r--compiler/Translate.ml2
1 files changed, 1 insertions, 1 deletions
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 *)