From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Thu, 30 Jun 2022 12:22:14 +0200
Subject: Traduct globals body separately (WIP)

---
 src/Translate.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/Translate.ml')

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
-- 
cgit v1.2.3