Regenerate the code

2 files changed, 24 insertions, 30 deletions

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index ab424e42..d709a8d5 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (List_t T) slots List_Nil;
+      slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashMap_allocate_slots_loop T n2 v n3)
+      hashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | List_Cons k v tl =>
-      hm <- hashMap_insert_no_resize T n1 ntable k v;
-      hashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
+      hashMap_move_elements_from_list_loop T n1 ntable1 tl
     | List_Nil => Return ntable
     end
   end
@@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop
           (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (List_t T) l List_Nil in
-      hm <- hashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -241,9 +239,7 @@ Definition hashMap_move_elements
   (slots : alloc_vec_Vec (List_t T)) (i : usize) :
   result ((HashMap_t T) * (alloc_vec_Vec (List_t T)))
   :=
-  back_'a <- hashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
@@ -284,9 +280,11 @@ Definition hashMap_insert
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
   :=
-  hm <- hashMap_insert_no_resize T n self key value;
-  i <- hashMap_len T hm;
-  if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm
+  self1 <- hashMap_insert_no_resize T n self key value;
+  i <- hashMap_len T self1;
+  if i s> self1.(hashMap_max_load)
+  then hashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index aff4995f..9fb3c482 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
+      slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashmap_HashMap_allocate_slots_loop T n2 v n3)
+      hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | Hashmap_List_Cons k v tl =>
-      hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
-      hashmap_HashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
+      hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
     | Hashmap_List_Nil => Return ntable
     end
   end
@@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop
           i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in
-      hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -256,9 +254,7 @@ Definition hashmap_HashMap_move_elements
   (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) :
   result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T)))
   :=
-  back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashmap_HashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
@@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert
   (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) :
   result (hashmap_HashMap_t T)
   :=
-  hm <- hashmap_HashMap_insert_no_resize T n self key value;
-  i <- hashmap_HashMap_len T hm;
-  if i s> hm.(hashmap_HashMap_max_load)
-  then hashmap_HashMap_try_resize T n hm
-  else Return hm
+  self1 <- hashmap_HashMap_insert_no_resize T n self key value;
+  i <- hashmap_HashMap_len T self1;
+  if i s> self1.(hashmap_HashMap_max_load)
+  then hashmap_HashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: