Merge branch 'main' into son/loops2

1 files changed, 9 insertions, 9 deletions

diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 2e74e21a..e2412076 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -6,12 +6,12 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [paper::ref_incr]:
-    Source: 'tests/src/paper.rs', lines 4:0-4:28 *)
+    Source: 'tests/src/paper.rs', lines 7:0-7:28 *)
 let ref_incr (x : i32) : result i32 =
   i32_add x 1
 
 (** [paper::test_incr]:
-    Source: 'tests/src/paper.rs', lines 8:0-8:18 *)
+    Source: 'tests/src/paper.rs', lines 11:0-11:18 *)
 let test_incr : result unit =
   let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Ok ()
 
@@ -19,7 +19,7 @@ let test_incr : result unit =
 let _ = assert_norm (test_incr = Ok ())
 
 (** [paper::choose]:
-    Source: 'tests/src/paper.rs', lines 15:0-15:70 *)
+    Source: 'tests/src/paper.rs', lines 18:0-18:70 *)
 let choose
   (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
   if b
@@ -27,7 +27,7 @@ let choose
   else let back = fun ret -> Ok (x, ret) in Ok (y, back)
 
 (** [paper::test_choose]:
-    Source: 'tests/src/paper.rs', lines 23:0-23:20 *)
+    Source: 'tests/src/paper.rs', lines 26:0-26:20 *)
 let test_choose : result unit =
   let* (z, choose_back) = choose i32 true 0 0 in
   let* z1 = i32_add z 1 in
@@ -43,13 +43,13 @@ let test_choose : result unit =
 let _ = assert_norm (test_choose = Ok ())
 
 (** [paper::List]
-    Source: 'tests/src/paper.rs', lines 35:0-35:16 *)
+    Source: 'tests/src/paper.rs', lines 38:0-38:16 *)
 type list_t (t : Type0) =
 | List_Cons : t -> list_t t -> list_t t
 | List_Nil : list_t t
 
 (** [paper::list_nth_mut]:
-    Source: 'tests/src/paper.rs', lines 42:0-42:67 *)
+    Source: 'tests/src/paper.rs', lines 45:0-45:67 *)
 let rec list_nth_mut
   (t : Type0) (l : list_t t) (i : u32) :
   result (t & (t -> result (list_t t)))
@@ -68,7 +68,7 @@ let rec list_nth_mut
   end
 
 (** [paper::sum]:
-    Source: 'tests/src/paper.rs', lines 57:0-57:32 *)
+    Source: 'tests/src/paper.rs', lines 60:0-60:32 *)
 let rec sum (l : list_t i32) : result i32 =
   begin match l with
   | List_Cons x tl -> let* i = sum tl in i32_add x i
@@ -76,7 +76,7 @@ let rec sum (l : list_t i32) : result i32 =
   end
 
 (** [paper::test_nth]:
-    Source: 'tests/src/paper.rs', lines 68:0-68:17 *)
+    Source: 'tests/src/paper.rs', lines 71:0-71:17 *)
 let test_nth : result unit =
   let l = List_Cons 3 List_Nil in
   let l1 = List_Cons 2 l in
@@ -90,7 +90,7 @@ let test_nth : result unit =
 let _ = assert_norm (test_nth = Ok ())
 
 (** [paper::call_choose]:
-    Source: 'tests/src/paper.rs', lines 76:0-76:44 *)
+    Source: 'tests/src/paper.rs', lines 79:0-79:44 *)
 let call_choose (p : (u32 & u32)) : result u32 =
   let (px, py) = p in
   let* (pz, choose_back) = choose u32 true px py in