summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index fba1dfb0..9af3c71b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -469,6 +469,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
groups are always singletons, so the [extract_global_decl] function
takes care of generating the delimiters.
*)
+ let global = SymbolicToPure.translate_global ctx.trans_ctx global in
Extract.extract_global_decl ctx fmt global body config.interface
(** Utility.