1 files changed, 21 insertions, 0 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
new file mode 100644
index 00000000..f41c3ddf
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
@@ -0,0 +1,21 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: opaque function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain__Types .
+Import HashmapMain__Types .
+Module HashmapMain__Opaque .
+
+(** [hashmap_main::hashmap_utils::deserialize] *)
+Axiom hashmap_utils_deserialize_fwd
+  : state -> result (state * (Hashmap_hash_map_t u64))
+  .
+
+(** [hashmap_main::hashmap_utils::serialize] *)
+Axiom hashmap_utils_serialize_fwd
+  : Hashmap_hash_map_t u64 -> state -> result (state * unit)
+  .
+
+End HashmapMain__Opaque .