diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/Paper.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 25c01d7b..d0c99883 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -13,7 +13,7 @@ Definition ref_incr_fwd_back (x : i32) : result i32 := (** [paper::test_incr] *) Definition test_incr_fwd : result unit := x <- ref_incr_fwd_back (0 %i32); - if negb (x s= 1 %i32) then Fail_ else Return tt + if negb (x s= 1 %i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_incr] *) @@ -33,13 +33,13 @@ Definition test_choose_fwd : result unit := z <- choose_fwd i32 true (0 %i32) (0 %i32); z0 <- i32_add z 1 %i32; if negb (z0 s= 1 %i32) - then Fail_ + then Fail_ Failure else ( p <- choose_back i32 true (0 %i32) (0 %i32) z0; let (x, y) := p in if negb (x s= 1 %i32) - then Fail_ - else if negb (y s= 0 %i32) then Fail_ else Return tt) + then Fail_ Failure + else if negb (y s= 0 %i32) then Fail_ Failure else Return tt) . (** Unit test for [paper::test_choose] *) @@ -61,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := if i s= 0 %u32 then Return x else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t) - | ListNil => Fail_ + | ListNil => Fail_ Failure end . @@ -76,7 +76,7 @@ Fixpoint list_nth_mut_back i0 <- u32_sub i 1 %u32; tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0)) - | ListNil => Fail_ + | ListNil => Fail_ Failure end . @@ -97,7 +97,7 @@ Definition test_nth_fwd : result unit := x0 <- i32_add x 1 %i32; l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0; i <- sum_fwd l2; - if negb (i s= 7 %i32) then Fail_ else Return tt + if negb (i s= 7 %i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_nth] *) |