diff options
Diffstat (limited to 'tests/coq/misc')
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 5 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 4 |
2 files changed, 2 insertions, 7 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 90390c1b..b5476f25 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -46,10 +46,7 @@ Definition test_new_non_zero_u32_fwd (** [external::test_vec] *) Definition test_vec_fwd : result unit := - let v := vec_new u32 in - v0 <- vec_push_back u32 v (0%u32); - let _ := v0 in - Return tt + let v := vec_new u32 in _ <- vec_push_back u32 v (0%u32); Return tt . (** Unit test for [external::test_vec] *) diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index e91cf81a..10654887 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -67,9 +67,7 @@ Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y. Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x. (** [no_nested_borrows::test2] *) -Definition test2_fwd : result unit := - i <- u32_add 23%u32 44%u32; let _ := i in Return tt -. +Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt. (** Unit test for [no_nested_borrows::test2] *) Check (test2_fwd )%return. |