From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/fstar/hashmap/Hashmap.Funs.fst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tests/fstar/hashmap')

diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 447f9b49..7ca8b9c1 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -308,8 +308,7 @@ let hashMap_get_mut_in_list
   (t : Type0) (ls : list_t t) (key : usize) :
   result (t & (t -> result (list_t t)))
   =
-  let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in
-  Return (x, back_'a)
+  hashMap_get_mut_in_list_loop t ls key
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut]:
     Source: 'src/hashmap.rs', lines 257:4-257:67 *)
-- 
cgit v1.2.3