From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

---
 tests/coq/misc/External_Funs.v   |  6 +++---
 tests/coq/misc/Loops.v           | 22 +++++++++++-----------
 tests/coq/misc/NoNestedBorrows.v |  9 ++-------
 tests/coq/misc/Paper.v           |  2 +-
 4 files changed, 17 insertions(+), 22 deletions(-)

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 91ea88c9..faf91fef 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -45,9 +45,9 @@ Definition custom_swap
   :=
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
-  let (t, t1) := p1 in
-  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in
-  Return (st1, (t, back_'a))
+  let (x1, y1) := p1 in
+  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+  Return (st1, (x1, back_'a))
 .
 
 (** [external::test_custom_swap]:
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 85b54510..7c83a014 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 :=
 (** [loops::sum_with_mut_borrows]: loop 0:
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 Fixpoint sum_with_mut_borrows_loop
-  (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if mi s< max
+    if i s< max
     then (
-      ms1 <- u32_add ms mi;
-      mi1 <- u32_add mi 1%u32;
-      sum_with_mut_borrows_loop n1 max mi1 ms1)
-    else u32_mul ms 2%u32
+      ms <- u32_add s i;
+      mi <- u32_add i 1%u32;
+      sum_with_mut_borrows_loop n1 max mi ms)
+    else u32_mul s 2%u32
   end
 .
 
@@ -245,10 +245,10 @@ Definition get_elem_mut
   p <-
     alloc_vec_Vec_index_mut (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  let (l, index_mut_back) := p in
-  p1 <- get_elem_mut_loop n x l;
+  let (ls, index_mut_back) := p in
+  p1 <- get_elem_mut_loop n x ls;
   let (i, back) := p1 in
-  let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+  let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
   Return (i, back1)
 .
 
@@ -273,10 +273,10 @@ Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
   :=
-  l <-
+  ls <-
     alloc_vec_Vec_index (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  get_elem_shared_loop n x l
+  get_elem_shared_loop n x ls
 .
 
 (** [loops::id_mut]:
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 73c4ee58..76dc4cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -475,9 +475,7 @@ Definition id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1)
-    in
-  Return ((x, y), back_'a)
+  Return ((x, y), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair2]:
@@ -486,10 +484,7 @@ Definition id_mut_pair2
   (T1 T2 : Type) (p : (T1 * T2)) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let (t, t1) := p in
-  let back_'a :=
-    fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in
-  Return ((t, t1), back_'a)
+  let (t, t1) := p in Return ((t, t1), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair3]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 769cf34c..ad77fa2a 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 Definition test_incr : result unit :=
-  i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt
+  x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
 .
 
 (** Unit test for [paper::test_incr] *)
-- 
cgit v1.2.3