From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:58:44 +0200
Subject: Regenerate the test files

---
 tests/coq/betree/BetreeMain_Funs.v                 | 12 ++--
 .../coq/betree/BetreeMain_FunsExternal_Template.v  |  3 +-
 tests/coq/demo/Demo.v                              | 28 ++++----
 tests/coq/hashmap/Hashmap_Funs.v                   | 18 ++---
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       | 17 +++--
 tests/coq/misc/External_Funs.v                     |  4 +-
 tests/coq/misc/External_FunsExternal_Template.v    |  9 ++-
 tests/coq/misc/External_TypesExternal_Template.v   |  3 +-
 tests/coq/misc/Loops.v                             | 78 +++++++++++-----------
 tests/coq/misc/NoNestedBorrows.v                   | 12 ++--
 tests/coq/misc/Paper.v                             | 12 ++--
 tests/coq/misc/PoloniusList.v                      |  4 +-
 tests/coq/traits/Traits.v                          |  3 +-
 13 files changed, 104 insertions(+), 99 deletions(-)

(limited to 'tests/coq')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c2cca26d..9256b149 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -240,11 +240,11 @@ Fixpoint betree_Node_lookup_first_message_for_key
       else (
         p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
         let (l, lookup_first_message_for_key_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_for_key_back ret;
             Return (Betree_List_Cons (i, m) next_msgs1) in
-        Return (l, back_'a))
+        Return (l, back))
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
@@ -440,11 +440,11 @@ Fixpoint betree_Node_lookup_first_message_after_key
       then (
         p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
         let (l, lookup_first_message_after_key_back) := p1 in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_after_key_back ret;
             Return (Betree_List_Cons (k, m) next_msgs1) in
-        Return (l, back_'a))
+        Return (l, back))
       else Return (Betree_List_Cons (k, m) next_msgs, Return)
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
@@ -550,11 +550,11 @@ Fixpoint betree_Node_lookup_mut_in_bindings
       else (
         p <- betree_Node_lookup_mut_in_bindings n1 key tl;
         let (l, lookup_mut_in_bindings_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * u64)) =>
             tl1 <- lookup_mut_in_bindings_back ret;
             Return (Betree_List_Cons (i, i1) tl1) in
-        Return (l, back_'a))
+        Return (l, back))
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index a9969448..1367bac2 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -38,7 +38,8 @@ Axiom betree_utils_store_leaf_node
 .
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index d5a6e535..abec8e88 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -13,8 +13,8 @@ Module Demo.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
-  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
 .
 
 (** [demo::mul2_add1]:
@@ -79,16 +79,16 @@ Fixpoint list_nth_mut
     | CList_CCons x tl =>
       if i s= 0%u32
       then
-        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut T n1 tl i1;
         let (t, list_nth_mut_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : T) =>
             tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
-        Return (t, back_'a))
+        Return (t, back))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -107,15 +107,15 @@ Fixpoint list_nth_mut1_loop
     | CList_CCons x tl =>
       if i s= 0%u32
       then
-        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut1_loop T n1 tl i1;
-        let (t, back_'a) := p in
-        let back_'a1 :=
-          fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in
-        Return (t, back_'a1))
+        let (t, back) := p in
+        let back1 :=
+          fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in
+        Return (t, back1))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -155,10 +155,10 @@ Fixpoint list_tail
     | CList_CCons t tl =>
       p <- list_tail T n1 tl;
       let (c, list_tail_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : CList_t T) =>
           tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
-      Return (c, back_'a)
+      Return (c, back)
     | CList_CNil => Return (CList_CNil, Return)
     end
   end
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d709a8d5..67543c8e 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -376,15 +376,15 @@ Fixpoint hashMap_get_mut_in_list_loop
     | List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back_'a := fun (ret : T) => Return (List_Cons ckey ret tl) in
-        Return (cvalue, back_'a)
+        let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
+        Return (cvalue, back)
       else (
         p <- hashMap_get_mut_in_list_loop T n1 tl key;
-        let (t, back_'a) := p in
-        let back_'a1 :=
-          fun (ret : T) =>
-            tl1 <- back_'a ret; Return (List_Cons ckey cvalue tl1) in
-        Return (t, back_'a1))
+        let (t, back) := p in
+        let back1 :=
+          fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
+          in
+        Return (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -415,7 +415,7 @@ Definition hashMap_get_mut
   let (l, index_mut_back) := p in
   p1 <- hashMap_get_mut_in_list T n l key;
   let (t, get_mut_in_list_back) := p1 in
-  let back_'a :=
+  let back :=
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
@@ -426,7 +426,7 @@ Definition hashMap_get_mut
           hashMap_max_load := self.(hashMap_max_load);
           hashMap_slots := v
         |} in
-  Return (t, back_'a)
+  Return (t, back)
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 9fb3c482..a614e52d 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -398,16 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back_'a := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl)
-          in
-        Return (cvalue, back_'a)
+        let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
+        Return (cvalue, back)
       else (
         p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
-        let (t, back_'a) := p in
-        let back_'a1 :=
+        let (t, back) := p in
+        let back1 :=
           fun (ret : T) =>
-            tl1 <- back_'a ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
-        Return (t, back_'a1))
+            tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
+        Return (t, back1))
     | Hashmap_List_Nil => Fail_ Failure
     end
   end
@@ -438,7 +437,7 @@ Definition hashmap_HashMap_get_mut
   let (l, index_mut_back) := p in
   p1 <- hashmap_HashMap_get_mut_in_list T n l key;
   let (t, get_mut_in_list_back) := p1 in
-  let back_'a :=
+  let back :=
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
@@ -450,7 +449,7 @@ Definition hashmap_HashMap_get_mut
           hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
           hashmap_HashMap_slots := v
         |} in
-  Return (t, back_'a)
+  Return (t, back)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index faf91fef..a6832854 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,8 +46,8 @@ Definition custom_swap
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
   let (x1, y1) := p1 in
-  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
-  Return (st1, (x1, back_'a))
+  let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+  Return (st1, (x1, back))
 .
 
 (** [external::test_custom_swap]:
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 6773ac18..24dd2d47 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,19 +12,22 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+    Name pattern: core::mem::swap *)
 Axiom core_mem_swap :
   forall(T : Type), T -> T -> state -> result (state * (T * T))
 .
 
 (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
 Axiom core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
 .
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7ba79d8e..7d6af202 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -10,7 +10,8 @@ Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
 (** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+    Name pattern: core::num::nonzero::NonZeroU32 *)
 Axiom core_num_nonzero_NonZeroU32_t : Type.
 
 (** The state type used in the state-error monad *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 7c83a014..ae529cf8 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'a, back_'b)
+          let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
+          let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back'a, back'b)
         else (
           i1 <- u32_sub i 1%u32;
           t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
-          let '(p, back_'a, back_'b) := t in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          let back_'b1 :=
-            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
-          Return (p, back_'a1, back_'b1))
+          let '(p, back'a, back'b) := t in
+          let back'a1 :=
+            fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+          let back'b1 :=
+            fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
+          Return (p, back'a1, back'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a :=
+          let back :=
             fun (ret : (T * T)) =>
               let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
             in
-          Return ((x0, x1), back_'a)
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
+          let (p1, back) := p in
+          let back1 :=
             fun (ret : (T * T)) =>
-              p2 <- back_'a ret;
+              p2 <- back ret;
               let (tl01, tl11) := p2 in
               Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-          Return (p1, back_'a1))
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'b)
+          let back := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
-          let (p1, back_'b) := p in
-          let back_'b1 :=
-            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
-          Return (p1, back_'b1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 76dc4cf6..d4035104 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -321,8 +321,8 @@ Check (test_split_list )%return.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
-  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
 .
 
 (** [no_nested_borrows::choose_test]:
@@ -399,16 +399,16 @@ Fixpoint list_nth_mut
   | List_Cons x tl =>
     if i s= 0%u32
     then
-      let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
-      Return (x, back_'a)
+      let back := fun (ret : T) => Return (List_Cons ret tl) in
+      Return (x, back)
     else (
       i1 <- u32_sub i 1%u32;
       p <- list_nth_mut T tl i1;
       let (t, list_nth_mut_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
         in
-      Return (t, back_'a))
+      Return (t, back))
   | List_Nil => Fail_ Failure
   end
 .
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index ad77fa2a..77276223 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -27,8 +27,8 @@ Check (test_incr )%return.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
-  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
 .
 
 (** [paper::test_choose]:
@@ -70,16 +70,16 @@ Fixpoint list_nth_mut
   | List_Cons x tl =>
     if i s= 0%u32
     then
-      let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
-      Return (x, back_'a)
+      let back := fun (ret : T) => Return (List_Cons ret tl) in
+      Return (x, back)
     else (
       i1 <- u32_sub i 1%u32;
       p <- list_nth_mut T tl i1;
       let (t, list_nth_mut_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
         in
-      Return (t, back_'a))
+      Return (t, back))
   | List_Nil => Fail_ Failure
   end
 .
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index 8f403a8e..dfa09328 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -31,10 +31,10 @@ Fixpoint get_list_at_x
     else (
       p <- get_list_at_x tl x;
       let (l, get_list_at_x_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : List_t u32) =>
           tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in
-      Return (l, back_'a))
+      Return (l, back))
   | List_Nil => Return (List_Nil, Return)
   end
 .
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index a861c114..0e942c7d 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -671,7 +671,8 @@ Arguments foo_x { _ _ }.
 Arguments foo_y { _ _ }.
 
 (** [core::result::Result]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+    Name pattern: core::result::Result *)
 Inductive core_result_Result_t (T E : Type) :=
 | Core_result_Result_Ok : T -> core_result_Result_t T E
 | Core_result_Result_Err : E -> core_result_Result_t T E
-- 
cgit v1.2.3


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