Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

1 files changed, 0 insertions, 25 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
deleted file mode 100644
index a0e9003d..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [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_Opaque.
-
-(** [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_Opaque .