diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 4 |
1 files changed, 1 insertions, 3 deletions
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] *) |