summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti')
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
index 78a6c3ba..d6cecf36 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
@@ -7,10 +7,10 @@ include HashmapMain.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [hashmap_main::hashmap_utils::deserialize]: forward function *)
-val hashmap_utils_deserialize_fwd
- : state -> result (state & (hashmap_hash_map_t u64))
+val hashmap_utils_deserialize
+ : state -> result (state & (hashmap_HashMap_t u64))
(** [hashmap_main::hashmap_utils::serialize]: forward function *)
-val hashmap_utils_serialize_fwd
- : hashmap_hash_map_t u64 -> state -> result (state & unit)
+val hashmap_utils_serialize
+ : hashmap_HashMap_t u64 -> state -> result (state & unit)