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/demo/Demo.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/coq/demo')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 48067c02..2fccf6c0 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -127,7 +127,7 @@ Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+  list_nth_mut1_loop T n l i
 .
 
 (** [demo::i32_id]:
-- 
cgit v1.2.3