From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types

---
 tests/fstar/misc/External.Types.fst          |  8 ++++++++
 tests/fstar/misc/External.Types.fsti         | 14 --------------
 tests/fstar/misc/External.TypesExternal.fsti | 14 ++++++++++++++
 3 files changed, 22 insertions(+), 14 deletions(-)
 create mode 100644 tests/fstar/misc/External.Types.fst
 delete mode 100644 tests/fstar/misc/External.Types.fsti
 create mode 100644 tests/fstar/misc/External.TypesExternal.fsti

(limited to 'tests/fstar/misc')

diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
new file mode 100644
index 00000000..4fbcec47
--- /dev/null
+++ b/tests/fstar/misc/External.Types.fst
@@ -0,0 +1,8 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+module External.Types
+open Primitives
+include External.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.Types.fsti
deleted file mode 100644
index 0cb9fd0e..00000000
--- a/tests/fstar/misc/External.Types.fsti
+++ /dev/null
@@ -1,14 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-val core_num_nonzero_NonZeroU32_t : Type0
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
new file mode 100644
index 00000000..4bfbe0c5
--- /dev/null
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -0,0 +1,14 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external type declarations *)
+module External.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+val core_num_nonzero_NonZeroU32_t : Type0
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
-- 
cgit v1.2.3