Generate a dedicated file for the external types

2 files changed, 11 insertions, 3 deletions

diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
index e77954ad..afebcde3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -2,6 +2,7 @@
 (** [hashmap_main]: type definitions *)
 module HashmapMain.Types
 open Primitives
+include HashmapMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) =
   slots : alloc_vec_Vec (hashmap_List_t t);
 }
 
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
new file mode 100644
index 00000000..75747408
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external type declarations *)
+module HashmapMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+