From a52939b5119e2751570582533bf27828724c2e9f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 01:18:37 +0100
Subject: Fix an issue when deconstructing tuples in Coq

---
 tests/coq/misc/Loops.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index cc76f359..af920d41 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -358,7 +358,7 @@ Fixpoint list_nth_mut_loop_pair_loop
         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 '(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 :=
@@ -378,7 +378,7 @@ Definition list_nth_mut_loop_pair
   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
+  let '(p, back_'a, back_'b) := t in
   Return (p, back_'a, back_'b)
 .
 
-- 
cgit v1.2.3