Improve the pretty names generation for loops

2 files changed, 12 insertions, 12 deletions

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 9c65fb46..0d55b171 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -131,8 +131,8 @@ Fixpoint hash_map_insert_in_list_loop_back
       if ckey s= key
       then Return (ListCons ckey value tl)
       else (
-        l <- hash_map_insert_in_list_loop_back T n0 key value tl;
-        Return (ListCons ckey cvalue l))
+        tl0 <- hash_map_insert_in_list_loop_back T n0 key value tl;
+        Return (ListCons ckey cvalue tl0))
     | ListNil => let l := ListNil in Return (ListCons key value l)
     end
   end
@@ -365,8 +365,8 @@ Fixpoint hash_map_get_mut_in_list_loop_back
       if ckey s= key
       then Return (ListCons ckey ret tl)
       else (
-        l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
-        Return (ListCons ckey cvalue l))
+        tl0 <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
+        Return (ListCons ckey cvalue tl0))
     | ListNil => Fail_ Failure
     end
   end
@@ -448,8 +448,8 @@ Fixpoint hash_map_remove_from_list_loop_back
         | ListNil => Fail_ Failure
         end
       else (
-        l <- hash_map_remove_from_list_loop_back T n0 key tl;
-        Return (ListCons ckey t l))
+        tl0 <- hash_map_remove_from_list_loop_back T n0 key tl;
+        Return (ListCons ckey t tl0))
     | ListNil => Return ListNil
     end
   end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 94a9e6a5..670e527a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -139,8 +139,8 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back
       if ckey s= key
       then Return (HashmapListCons ckey value tl)
       else (
-        l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
-        Return (HashmapListCons ckey cvalue l))
+        tl0 <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
+        Return (HashmapListCons ckey cvalue tl0))
     | HashmapListNil =>
       let l := HashmapListNil in Return (HashmapListCons key value l)
     end
@@ -391,8 +391,8 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
       if ckey s= key
       then Return (HashmapListCons ckey ret tl)
       else (
-        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
-        Return (HashmapListCons ckey cvalue l))
+        tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
+        Return (HashmapListCons ckey cvalue tl0))
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -490,8 +490,8 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
         | HashmapListNil => Fail_ Failure
         end
       else (
-        l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
-        Return (HashmapListCons ckey t l))
+        tl0 <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
+        Return (HashmapListCons ckey t tl0))
     | HashmapListNil => Return HashmapListNil
     end
   end