summaryrefslogtreecommitdiff
path: root/tests/fstar-split/misc/External.Funs.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar-split/misc/External.Funs.fst')
-rw-r--r--tests/fstar-split/misc/External.Funs.fst4
1 files changed, 1 insertions, 3 deletions
diff --git a/tests/fstar-split/misc/External.Funs.fst b/tests/fstar-split/misc/External.Funs.fst
index 3b84697e..65382549 100644
--- a/tests/fstar-split/misc/External.Funs.fst
+++ b/tests/fstar-split/misc/External.Funs.fst
@@ -36,9 +36,7 @@ let test_new_non_zero_u32
(** [external::test_vec]: forward function
Source: 'src/external.rs', lines 17:0-17:17 *)
let test_vec : result unit =
- let v = alloc_vec_Vec_new u32 in
- let* _ = alloc_vec_Vec_push u32 v 0 in
- Return ()
+ let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Return ()
(** Unit test for [external::test_vec] *)
let _ = assert_norm (test_vec = Return ())