`extern` globals declared in bundles should move to `internal/*.h`

[tahina-pro]

Consider the following modules, Test.Hidden and Test:

module Test.Hidden
module U32 = FStar.UInt32
noeq type t = { a: U32.t; b: U32.t; }
assume val g (_: unit) : Tot U32.t
let x = { a = 18ul; b = g (); }

module Test
let f () = Test.Hidden.x.a

Then, when I run krml Test.Hidden.fst Test.fst -skip-compilation -bundle Test=Test.Hidden, I obtain this in Test.h:

extern Test_Hidden_t Test_Hidden_x;

Should this global variable declaration rather go to internal/Test.h? I was expecting it not to appear on the top-level interface, since x is defined in Test.Hidden, which is in a bundle. Indeed if I replace the call to g with a constant, x properly disappears from the interface and directly goes into Test.c.

Sealing Test.Hidden behind an interface (hiding x in the implementation and replacing it in the interface with a function signature, implemented in the .fst to access it) does not help.

Thank you in advance!