From a4decc7654bc6f3301c0174124d21fdbc2dbc708 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 00:59:55 +0100
Subject: Regenerate the files

---
 tests/coq/misc/External_Funs.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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

diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 049f5d39..91ea88c9 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -31,9 +31,7 @@ Definition test_new_non_zero_u32
 (** [external::test_vec]:
     Source: 'src/external.rs', lines 17:0-17:17 *)
 Definition test_vec : result unit :=
-  let v := alloc_vec_Vec_new u32 in
-  _ <- alloc_vec_Vec_push u32 v 0%u32;
-  Return tt
+  _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Return tt
 .
 
 (** Unit test for [external::test_vec] *)
-- 
cgit v1.2.3