From 3e719defdd22b0e6c4bedce8996c2a58bb77a783 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 5 Mar 2022 17:12:22 +0100
Subject: Make an update in the hash map

---
 tests/hashmap/Hashmap.Funs.fst             | 6 ++----
 tests/hashmap_on_disk/HashmapMain.Funs.fst | 7 ++-----
 2 files changed, 4 insertions(+), 9 deletions(-)

(limited to 'tests')

diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 75cd1659..5a987799 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -264,11 +264,9 @@ let hash_map_try_resize_fwd_back
             begin match
               hash_map_move_elements_fwd_back t hm self.hash_map_slots 0 with
             | Fail -> Fail
-            | Return (hm0, v) ->
-              let v0 = mem_replace_back (vec (list_t t)) v hm0.hash_map_slots
-                in
+            | Return (hm0, _) ->
               Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
-                hm0.hash_map_max_load v0)
+                hm0.hash_map_max_load hm0.hash_map_slots)
             end
           end
         end
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 0eda588f..89b9ef5b 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -447,13 +447,10 @@ let hashmap_hash_map_try_resize_back
               hashmap_hash_map_move_elements_back t hm
                 self.hashmap_hash_map_slots 0 st0 with
             | Fail -> Fail
-            | Return (st1, (hm0, v)) ->
-              let v0 =
-                mem_replace_back (vec (hashmap_list_t t)) v
-                  hm0.hashmap_hash_map_slots in
+            | Return (st1, (hm0, _)) ->
               Return (st1, Mkhashmap_hash_map_t
                 self.hashmap_hash_map_num_entries (i0, i1)
-                hm0.hashmap_hash_map_max_load v0)
+                hm0.hashmap_hash_map_max_load hm0.hashmap_hash_map_slots)
             end
           end
         end
-- 
cgit v1.2.3