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/NoNestedBorrows.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'tests/coq/misc/NoNestedBorrows.v')

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]:
-- 
cgit v1.2.3