Regenerate the test files

2 files changed, 12 insertions, 12 deletions

diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 0e770ac9..d897933a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -79,8 +79,8 @@ let rec hashMap_clear_loop
 (** [hashmap::{hashmap::HashMap<T>}::clear]:
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
-  let* back = hashMap_clear_loop t self.slots 0 in
-  Return { self with num_entries = 0; slots = back }
+  let* hm = hashMap_clear_loop t self.slots 0 in
+  Return { self with num_entries = 0; slots = hm }
 
 (** [hashmap::{hashmap::HashMap<T>}::len]:
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop
     if ckey = key
     then Return (false, List_Cons ckey value tl)
     else
-      let* (b, back) = hashMap_insert_in_list_loop t key value tl in
-      Return (b, List_Cons ckey cvalue back)
+      let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in
+      Return (b, List_Cons ckey cvalue tl1)
   | List_Nil -> Return (true, List_Cons key value List_Nil)
   end
 
@@ -344,8 +344,8 @@ let rec hashMap_remove_from_list_loop
       | List_Nil -> Fail Failure
       end
     else
-      let* (o, back) = hashMap_remove_from_list_loop t key tl in
-      Return (o, List_Cons ckey x back)
+      let* (o, tl1) = hashMap_remove_from_list_loop t key tl in
+      Return (o, List_Cons ckey x tl1)
   | List_Nil -> Return (None, List_Nil)
   end
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 09928620..e0005c81 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 let hashmap_HashMap_clear
   (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) =
-  let* back = hashmap_HashMap_clear_loop t self.slots 0 in
-  Return { self with num_entries = 0; slots = back }
+  let* hm = hashmap_HashMap_clear_loop t self.slots 0 in
+  Return { self with num_entries = 0; slots = hm }
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop
     if ckey = key
     then Return (false, Hashmap_List_Cons ckey value tl)
     else
-      let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in
-      Return (b, Hashmap_List_Cons ckey cvalue back)
+      let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in
+      Return (b, Hashmap_List_Cons ckey cvalue tl1)
   | Hashmap_List_Nil ->
     Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
   end
@@ -364,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop
       | Hashmap_List_Nil -> Fail Failure
       end
     else
-      let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in
-      Return (o, Hashmap_List_Cons ckey x back)
+      let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in
+      Return (o, Hashmap_List_Cons ckey x tl1)
   | Hashmap_List_Nil -> Return (None, Hashmap_List_Nil)
   end