diff options
author | Sidney Congard | 2022-06-30 12:22:14 +0200 |
---|---|---|
committer | Sidney Congard | 2022-06-30 12:22:14 +0200 |
commit | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (patch) | |
tree | 06ac570c7f9eee49987d716e043415ae31c681d0 /src/Translate.ml | |
parent | da118da3e590fbea4e880121837da2ee938837f6 (diff) |
Traduct globals body separately (WIP)
Diffstat (limited to 'src/Translate.ml')
-rw-r--r-- | src/Translate.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index d4d79355..9412b8b8 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -495,9 +495,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then - ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause def) + then if def.is_global + then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def + else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def + ) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then |