From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/coq/misc/Loops.v | 39 ++++++++++-----------------------------
 1 file changed, 10 insertions(+), 29 deletions(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e235b60d..85b54510 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -183,7 +183,7 @@ Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
+  list_nth_mut_loop_loop T n ls i
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
@@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
-  t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
-  let '(p, back_'a, back_'b) := t in
-  Return (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
   :=
-  p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'b) := p in
-  Return (p1, back_'b)
+  list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
@@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- incr_ignore_input_mut_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- ignore_input_shared_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
     else Return tt
   end
 .
-- 
cgit v1.2.3