From 5a96e28b8706ed945ccbb569881ca1888cd73ace Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 11:58:31 +0100
Subject: Regenerate the files and fix the proofs

---
 tests/coq/misc/Paper.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

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

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] *)
-- 
cgit v1.2.3