Improve the pretty names generation for loops

6 files changed, 47 insertions, 47 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
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ec77e4dd..bcbfc8df 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -147,8 +147,8 @@ Fixpoint list_nth_mut_loop_loop_back
       then Return (ListCons ret tl)
       else (
         i0 <- u32_sub i 1%u32;
-        l <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
-        Return (ListCons x l))
+        tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
+        Return (ListCons x tl0))
     | ListNil => Fail_ Failure
     end
   end
@@ -217,7 +217,7 @@ Fixpoint get_elem_mut_loop_back
     | ListCons y tl =>
       if y s= x
       then Return (ListCons ret tl)
-      else (l <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y l))
+      else (tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y tl0))
     | ListNil => Fail_ Failure
     end
   end
@@ -307,8 +307,8 @@ Fixpoint list_nth_mut_loop_with_id_loop_back
       then Return (ListCons ret tl)
       else (
         i0 <- u32_sub i 1%u32;
-        l <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
-        Return (ListCons x l))
+        tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
+        Return (ListCons x tl0))
     | ListNil => Fail_ Failure
     end
   end
@@ -395,8 +395,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l))
+          tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -428,8 +428,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l))
+          tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 tl10))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -527,8 +527,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back
         else (
           i0 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          let (l, l0) := p in
-          Return (ListCons x0 l, ListCons x1 l0))
+          let (tl00, tl10) := p in
+          Return (ListCons x0 tl00, ListCons x1 tl10))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -625,8 +625,8 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l))
+          tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -690,9 +690,9 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l <-
+          tl00 <-
             list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l))
+          Return (ListCons x0 tl00))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -756,8 +756,8 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l))
+          tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 tl10))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -821,9 +821,9 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l <-
+          tl10 <-
             list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l))
+          Return (ListCons x1 tl10))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 2074d02e..7137e92a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -128,7 +128,7 @@ let rec hash_map_insert_in_list_loop_back
     else
       begin match hash_map_insert_in_list_loop_back t key value tl with
       | Fail e -> Fail e
-      | Return l -> Return (ListCons ckey cvalue l)
+      | Return tl0 -> Return (ListCons ckey cvalue tl0)
       end
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
@@ -413,7 +413,7 @@ let rec hash_map_get_mut_in_list_loop_back
     else
       begin match hash_map_get_mut_in_list_loop_back t tl key ret with
       | Fail e -> Fail e
-      | Return l -> Return (ListCons ckey cvalue l)
+      | Return tl0 -> Return (ListCons ckey cvalue tl0)
       end
   | ListNil -> Fail Failure
   end
@@ -514,7 +514,7 @@ let rec hash_map_remove_from_list_loop_back
     else
       begin match hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
-      | Return l -> Return (ListCons ckey x l)
+      | Return tl0 -> Return (ListCons ckey x tl0)
       end
   | ListNil -> Return ListNil
   end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index d2b87305..f3b480c3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -137,7 +137,7 @@ let rec hashmap_hash_map_insert_in_list_loop_back
     else
       begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with
       | Fail e -> Fail e
-      | Return l -> Return (HashmapListCons ckey cvalue l)
+      | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
       end
   | HashmapListNil ->
     let l = HashmapListNil in Return (HashmapListCons key value l)
@@ -442,7 +442,7 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
     else
       begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with
       | Fail e -> Fail e
-      | Return l -> Return (HashmapListCons ckey cvalue l)
+      | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
       end
   | HashmapListNil -> Fail Failure
   end
@@ -553,7 +553,7 @@ let rec hashmap_hash_map_remove_from_list_loop_back
     else
       begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
-      | Return l -> Return (HashmapListCons ckey x l)
+      | Return tl0 -> Return (HashmapListCons ckey x tl0)
       end
   | HashmapListNil -> Return HashmapListNil
   end
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 73539cf6..3e8425dd 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -140,7 +140,7 @@ let rec list_nth_mut_loop_loop_back
       | Return i0 ->
         begin match list_nth_mut_loop_loop_back t tl i0 ret with
         | Fail e -> Fail e
-        | Return l -> Return (ListCons x l)
+        | Return tl0 -> Return (ListCons x tl0)
         end
       end
   | ListNil -> Fail Failure
@@ -201,7 +201,7 @@ let rec get_elem_mut_loop_back
     else
       begin match get_elem_mut_loop_back x tl ret with
       | Fail e -> Fail e
-      | Return l -> Return (ListCons y l)
+      | Return tl0 -> Return (ListCons y tl0)
       end
   | ListNil -> Fail Failure
   end
@@ -290,7 +290,7 @@ let rec list_nth_mut_loop_with_id_loop_back
       | Return i0 ->
         begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with
         | Fail e -> Fail e
-        | Return l -> Return (ListCons x l)
+        | Return tl0 -> Return (ListCons x tl0)
         end
       end
   | ListNil -> Fail Failure
@@ -379,7 +379,7 @@ let rec list_nth_mut_loop_pair_loop_back'a
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x0 l)
+          | Return tl00 -> Return (ListCons x0 tl00)
           end
         end
     | ListNil -> Fail Failure
@@ -412,7 +412,7 @@ let rec list_nth_mut_loop_pair_loop_back'b
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x1 l)
+          | Return tl10 -> Return (ListCons x1 tl10)
           end
         end
     | ListNil -> Fail Failure
@@ -500,7 +500,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back
           begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0)
+          | Return (tl00, tl10) -> Return (ListCons x0 tl00, ListCons x1 tl10)
           end
         end
     | ListNil -> Fail Failure
@@ -588,7 +588,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back
           begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x0 l)
+          | Return tl00 -> Return (ListCons x0 tl00)
           end
         end
     | ListNil -> Fail Failure
@@ -650,7 +650,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
           begin match
             list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x0 l)
+          | Return tl00 -> Return (ListCons x0 tl00)
           end
         end
     | ListNil -> Fail Failure
@@ -711,7 +711,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back
           begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x1 l)
+          | Return tl10 -> Return (ListCons x1 tl10)
           end
         end
     | ListNil -> Fail Failure
@@ -773,7 +773,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
           begin match
             list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l -> Return (ListCons x1 l)
+          | Return tl10 -> Return (ListCons x1 tl10)
           end
         end
     | ListNil -> Fail Failure