summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hashmap')
-rw-r--r--tests/hashmap/Hashmap.Funs.fst6
1 files changed, 2 insertions, 4 deletions
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index f75a0c01..4fb9c8e4 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -181,8 +181,7 @@ let hash_map_insert_no_resize_fwd_back
| Fail -> Fail
| Return v ->
Return (Mkhash_map_t self.hash_map_num_entries
- self.hash_map_max_load_factor self.hash_map_max_load
- v)
+ self.hash_map_max_load_factor self.hash_map_max_load v)
end
end
end
@@ -574,8 +573,7 @@ let hash_map_remove_back
| Fail -> Fail
| Return v ->
Return (Mkhash_map_t self.hash_map_num_entries
- self.hash_map_max_load_factor self.hash_map_max_load
- v)
+ self.hash_map_max_load_factor self.hash_map_max_load v)
end
end
| Some x0 ->