From 46f64c1b9f3bfc2703186b32a74c611e0e43f63f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:21:47 +0200
Subject: Regenerate the test files

---
 tests/coq/hashmap/Hashmap_Funs.v             | 12 ++++++------
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 ++++++------
 2 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'tests/coq')

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 67543c8e..c0cde78d 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -94,13 +94,13 @@ Fixpoint hashMap_clear_loop
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 Definition hashMap_clear
   (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
-  back <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
+  hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
   Return
     {|
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := self.(hashMap_max_load_factor);
       hashMap_max_load := self.(hashMap_max_load);
-      hashMap_slots := back
+      hashMap_slots := hm
     |}
 .
 
@@ -125,8 +125,8 @@ Fixpoint hashMap_insert_in_list_loop
       then Return (false, List_Cons ckey value tl)
       else (
         p <- hashMap_insert_in_list_loop T n1 key value tl;
-        let (b, back) := p in
-        Return (b, List_Cons ckey cvalue back))
+        let (b, tl1) := p in
+        Return (b, List_Cons ckey cvalue tl1))
     | List_Nil => Return (true, List_Cons key value List_Nil)
     end
   end
@@ -450,8 +450,8 @@ Fixpoint hashMap_remove_from_list_loop
         end
       else (
         p <- hashMap_remove_from_list_loop T n1 key tl;
-        let (o, back) := p in
-        Return (o, List_Cons ckey t back))
+        let (o, tl1) := p in
+        Return (o, List_Cons ckey t tl1))
     | List_Nil => Return (None, List_Nil)
     end
   end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index a614e52d..8e299800 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -104,13 +104,13 @@ Definition hashmap_HashMap_clear
   (T : Type) (n : nat) (self : hashmap_HashMap_t T) :
   result (hashmap_HashMap_t T)
   :=
-  back <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
+  hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
   Return
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
       hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
-      hashmap_HashMap_slots := back
+      hashmap_HashMap_slots := hm
     |}
 .
 
@@ -136,8 +136,8 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
       then Return (false, Hashmap_List_Cons ckey value tl)
       else (
         p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
-        let (b, back) := p in
-        Return (b, Hashmap_List_Cons ckey cvalue back))
+        let (b, tl1) := p in
+        Return (b, Hashmap_List_Cons ckey cvalue tl1))
     | Hashmap_List_Nil =>
       Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
     end
@@ -474,8 +474,8 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
         end
       else (
         p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
-        let (o, back) := p in
-        Return (o, Hashmap_List_Cons ckey t back))
+        let (o, tl1) := p in
+        Return (o, Hashmap_List_Cons ckey t tl1))
     | Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
     end
   end
-- 
cgit v1.2.3