diff options
| author | Son HO | 2024-03-18 07:23:00 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-18 07:23:00 +0100 |
| commit | a24f42ff7f0ae3c2aeb51decb0d0c90d6e50ffac (patch) | |
| tree | 7c9e526912d4fcbde4ed2ff4c17988fd5c89c96e /compiler/Translate.ml | |
| parent | d56946242859e0d375c1d44585b9da6d5fbe94cb (diff) | |
| parent | 9e230d0c4378b5c992c820cc1f4322896f739095 (diff) | |
Merge pull request #92 from AeneasVerif/son/globals
Add generics to constants/globals
Diffstat (limited to '')
| -rw-r--r-- | compiler/Translate.ml | 1 |
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. |