Merge branch 'main' into unsigned-max

1 files changed, 0 insertions, 24 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
deleted file mode 100644
index fb5f23cd..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
+++ /dev/null
@@ -1,24 +0,0 @@
-(** [hashmap_main]: external function declarations *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
-Module HashmapMain_FunsExternal.
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
-Axiom hashmap_utils_deserialize
-  : state -> result (state * (hashmap_HashMap_t u64))
-.
-
-(** [hashmap_main::hashmap_utils::serialize]: forward function
-    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
-Axiom hashmap_utils_serialize
-  : hashmap_HashMap_t u64 -> state -> result (state * unit)
-.
-
-End HashmapMain_FunsExternal.