Merge branch 'main' into unsigned-max

1 files changed, 49 insertions, 49 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index bf0a8bc1..87b05193 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module Loops.
 
 (** [loops::sum]: loop 0:
-    Source: 'tests/src/loops.rs', lines 4:0-14:1 *)
+    Source: 'tests/src/loops.rs', lines 8:0-18:1 *)
 Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -21,13 +21,13 @@ Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
 .
 
 (** [loops::sum]:
-    Source: 'tests/src/loops.rs', lines 4:0-4:27 *)
+    Source: 'tests/src/loops.rs', lines 8:0-8:27 *)
 Definition sum (n : nat) (max : u32) : result u32 :=
   sum_loop n max 0%u32 0%u32
 .
 
 (** [loops::sum_with_mut_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 19:0-31:1 *)
+    Source: 'tests/src/loops.rs', lines 23:0-35:1 *)
 Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -43,13 +43,13 @@ Fixpoint sum_with_mut_borrows_loop
 .
 
 (** [loops::sum_with_mut_borrows]:
-    Source: 'tests/src/loops.rs', lines 19:0-19:44 *)
+    Source: 'tests/src/loops.rs', lines 23:0-23:44 *)
 Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 :=
   sum_with_mut_borrows_loop n max 0%u32 0%u32
 .
 
 (** [loops::sum_with_shared_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 34:0-48:1 *)
+    Source: 'tests/src/loops.rs', lines 38:0-52:1 *)
 Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -65,13 +65,13 @@ Fixpoint sum_with_shared_borrows_loop
 .
 
 (** [loops::sum_with_shared_borrows]:
-    Source: 'tests/src/loops.rs', lines 34:0-34:47 *)
+    Source: 'tests/src/loops.rs', lines 38:0-38:47 *)
 Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
   sum_with_shared_borrows_loop n max 0%u32 0%u32
 .
 
 (** [loops::sum_array]: loop 0:
-    Source: 'tests/src/loops.rs', lines 50:0-58:1 *)
+    Source: 'tests/src/loops.rs', lines 54:0-62:1 *)
 Fixpoint sum_array_loop
   (N : usize) (n : nat) (a : array u32 N) (i : usize) (s : u32) : result u32 :=
   match n with
@@ -88,13 +88,13 @@ Fixpoint sum_array_loop
 .
 
 (** [loops::sum_array]:
-    Source: 'tests/src/loops.rs', lines 50:0-50:52 *)
+    Source: 'tests/src/loops.rs', lines 54:0-54:52 *)
 Definition sum_array (N : usize) (n : nat) (a : array u32 N) : result u32 :=
   sum_array_loop N n a 0%usize 0%u32
 .
 
 (** [loops::clear]: loop 0:
-    Source: 'tests/src/loops.rs', lines 62:0-68:1 *)
+    Source: 'tests/src/loops.rs', lines 66:0-72:1 *)
 Fixpoint clear_loop
   (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with
@@ -115,14 +115,14 @@ Fixpoint clear_loop
 .
 
 (** [loops::clear]:
-    Source: 'tests/src/loops.rs', lines 62:0-62:30 *)
+    Source: 'tests/src/loops.rs', lines 66:0-66:30 *)
 Definition clear
   (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) :=
   clear_loop n v 0%usize
 .
 
 (** [loops::List]
-    Source: 'tests/src/loops.rs', lines 70:0-70:16 *)
+    Source: 'tests/src/loops.rs', lines 74:0-74:16 *)
 Inductive List_t (T : Type) :=
 | List_Cons : T -> List_t T -> List_t T
 | List_Nil : List_t T
@@ -132,7 +132,7 @@ Arguments List_Cons { _ }.
 Arguments List_Nil { _ }.
 
 (** [loops::list_mem]: loop 0:
-    Source: 'tests/src/loops.rs', lines 76:0-85:1 *)
+    Source: 'tests/src/loops.rs', lines 80:0-89:1 *)
 Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
@@ -145,13 +145,13 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
 .
 
 (** [loops::list_mem]:
-    Source: 'tests/src/loops.rs', lines 76:0-76:52 *)
+    Source: 'tests/src/loops.rs', lines 80:0-80:52 *)
 Definition list_mem (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   list_mem_loop n x ls
 .
 
 (** [loops::list_nth_mut_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 88:0-98:1 *)
+    Source: 'tests/src/loops.rs', lines 92:0-102:1 *)
 Fixpoint list_nth_mut_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
@@ -175,7 +175,7 @@ Fixpoint list_nth_mut_loop_loop
 .
 
 (** [loops::list_nth_mut_loop]:
-    Source: 'tests/src/loops.rs', lines 88:0-88:71 *)
+    Source: 'tests/src/loops.rs', lines 92:0-92:71 *)
 Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
@@ -184,7 +184,7 @@ Definition list_nth_mut_loop
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 101:0-111:1 *)
+    Source: 'tests/src/loops.rs', lines 105:0-115:1 *)
 Fixpoint list_nth_shared_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -201,14 +201,14 @@ Fixpoint list_nth_shared_loop_loop
 .
 
 (** [loops::list_nth_shared_loop]:
-    Source: 'tests/src/loops.rs', lines 101:0-101:66 *)
+    Source: 'tests/src/loops.rs', lines 105:0-105:66 *)
 Definition list_nth_shared_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   list_nth_shared_loop_loop T n ls i
 .
 
 (** [loops::get_elem_mut]: loop 0:
-    Source: 'tests/src/loops.rs', lines 113:0-127:1 *)
+    Source: 'tests/src/loops.rs', lines 117:0-131:1 *)
 Fixpoint get_elem_mut_loop
   (n : nat) (x : usize) (ls : List_t usize) :
   result (usize * (usize -> result (List_t usize)))
@@ -233,7 +233,7 @@ Fixpoint get_elem_mut_loop
 .
 
 (** [loops::get_elem_mut]:
-    Source: 'tests/src/loops.rs', lines 113:0-113:73 *)
+    Source: 'tests/src/loops.rs', lines 117:0-117:73 *)
 Definition get_elem_mut
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result (usize * (usize -> result (alloc_vec_Vec (List_t usize))))
@@ -249,7 +249,7 @@ Definition get_elem_mut
 .
 
 (** [loops::get_elem_shared]: loop 0:
-    Source: 'tests/src/loops.rs', lines 129:0-143:1 *)
+    Source: 'tests/src/loops.rs', lines 133:0-147:1 *)
 Fixpoint get_elem_shared_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -263,7 +263,7 @@ Fixpoint get_elem_shared_loop
 .
 
 (** [loops::get_elem_shared]:
-    Source: 'tests/src/loops.rs', lines 129:0-129:68 *)
+    Source: 'tests/src/loops.rs', lines 133:0-133:68 *)
 Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
@@ -275,7 +275,7 @@ Definition get_elem_shared
 .
 
 (** [loops::id_mut]:
-    Source: 'tests/src/loops.rs', lines 145:0-145:50 *)
+    Source: 'tests/src/loops.rs', lines 149:0-149:50 *)
 Definition id_mut
   (T : Type) (ls : List_t T) :
   result ((List_t T) * (List_t T -> result (List_t T)))
@@ -284,12 +284,12 @@ Definition id_mut
 .
 
 (** [loops::id_shared]:
-    Source: 'tests/src/loops.rs', lines 149:0-149:45 *)
+    Source: 'tests/src/loops.rs', lines 153:0-153:45 *)
 Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
   Ok ls.
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 154:0-165:1 *)
+    Source: 'tests/src/loops.rs', lines 158:0-169:1 *)
 Fixpoint list_nth_mut_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) :
   result (T * (T -> result (List_t T)))
@@ -313,7 +313,7 @@ Fixpoint list_nth_mut_loop_with_id_loop
 .
 
 (** [loops::list_nth_mut_loop_with_id]:
-    Source: 'tests/src/loops.rs', lines 154:0-154:75 *)
+    Source: 'tests/src/loops.rs', lines 158:0-158:75 *)
 Definition list_nth_mut_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
@@ -327,7 +327,7 @@ Definition list_nth_mut_loop_with_id
 .
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 168:0-179:1 *)
+    Source: 'tests/src/loops.rs', lines 172:0-183:1 *)
 Fixpoint list_nth_shared_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -345,14 +345,14 @@ Fixpoint list_nth_shared_loop_with_id_loop
 .
 
 (** [loops::list_nth_shared_loop_with_id]:
-    Source: 'tests/src/loops.rs', lines 168:0-168:70 *)
+    Source: 'tests/src/loops.rs', lines 172:0-172:70 *)
 Definition list_nth_shared_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   ls1 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls1
 .
 
 (** [loops::list_nth_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 184:0-205:1 *)
+    Source: 'tests/src/loops.rs', lines 188:0-209:1 *)
 Fixpoint list_nth_mut_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
@@ -386,7 +386,7 @@ Fixpoint list_nth_mut_loop_pair_loop
 .
 
 (** [loops::list_nth_mut_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 184:0-188:27 *)
+    Source: 'tests/src/loops.rs', lines 188:0-192:27 *)
 Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
@@ -395,7 +395,7 @@ Definition list_nth_mut_loop_pair
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 208:0-229:1 *)
+    Source: 'tests/src/loops.rs', lines 212:0-233:1 *)
 Fixpoint list_nth_shared_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -419,7 +419,7 @@ Fixpoint list_nth_shared_loop_pair_loop
 .
 
 (** [loops::list_nth_shared_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 208:0-212:19 *)
+    Source: 'tests/src/loops.rs', lines 212:0-216:19 *)
 Definition list_nth_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -428,7 +428,7 @@ Definition list_nth_shared_loop_pair
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 233:0-248:1 *)
+    Source: 'tests/src/loops.rs', lines 237:0-252:1 *)
 Fixpoint list_nth_mut_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
@@ -464,7 +464,7 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 233:0-237:27 *)
+    Source: 'tests/src/loops.rs', lines 237:0-241:27 *)
 Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
@@ -473,7 +473,7 @@ Definition list_nth_mut_loop_pair_merge
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 251:0-266:1 *)
+    Source: 'tests/src/loops.rs', lines 255:0-270:1 *)
 Fixpoint list_nth_shared_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -498,7 +498,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 251:0-255:19 *)
+    Source: 'tests/src/loops.rs', lines 255:0-259:19 *)
 Definition list_nth_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -507,7 +507,7 @@ Definition list_nth_shared_loop_pair_merge
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 269:0-284:1 *)
+    Source: 'tests/src/loops.rs', lines 273:0-288:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -538,7 +538,7 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 269:0-273:23 *)
+    Source: 'tests/src/loops.rs', lines 273:0-277:23 *)
 Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -547,7 +547,7 @@ Definition list_nth_mut_shared_loop_pair
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 288:0-303:1 *)
+    Source: 'tests/src/loops.rs', lines 292:0-307:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -578,7 +578,7 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 288:0-292:23 *)
+    Source: 'tests/src/loops.rs', lines 292:0-296:23 *)
 Definition list_nth_mut_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -587,7 +587,7 @@ Definition list_nth_mut_shared_loop_pair_merge
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 307:0-322:1 *)
+    Source: 'tests/src/loops.rs', lines 311:0-326:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -618,7 +618,7 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 307:0-311:23 *)
+    Source: 'tests/src/loops.rs', lines 311:0-315:23 *)
 Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -627,7 +627,7 @@ Definition list_nth_shared_mut_loop_pair
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 326:0-341:1 *)
+    Source: 'tests/src/loops.rs', lines 330:0-345:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -658,7 +658,7 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 326:0-330:23 *)
+    Source: 'tests/src/loops.rs', lines 330:0-334:23 *)
 Definition list_nth_shared_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -667,7 +667,7 @@ Definition list_nth_shared_mut_loop_pair_merge
 .
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 345:0-349:1 *)
+    Source: 'tests/src/loops.rs', lines 349:0-353:1 *)
 Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
@@ -679,14 +679,14 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
 .
 
 (** [loops::ignore_input_mut_borrow]:
-    Source: 'tests/src/loops.rs', lines 345:0-345:56 *)
+    Source: 'tests/src/loops.rs', lines 349:0-349:56 *)
 Definition ignore_input_mut_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
   _ <- ignore_input_mut_borrow_loop n i; Ok _a
 .
 
 (** [loops::incr_ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 353:0-358:1 *)
+    Source: 'tests/src/loops.rs', lines 357:0-362:1 *)
 Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
@@ -698,14 +698,14 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
 .
 
 (** [loops::incr_ignore_input_mut_borrow]:
-    Source: 'tests/src/loops.rs', lines 353:0-353:60 *)
+    Source: 'tests/src/loops.rs', lines 357:0-357:60 *)
 Definition incr_ignore_input_mut_borrow
   (n : nat) (a : u32) (i : u32) : result u32 :=
   a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1
 .
 
 (** [loops::ignore_input_shared_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 362:0-366:1 *)
+    Source: 'tests/src/loops.rs', lines 366:0-370:1 *)
 Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
@@ -717,7 +717,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
 .
 
 (** [loops::ignore_input_shared_borrow]:
-    Source: 'tests/src/loops.rs', lines 362:0-362:59 *)
+    Source: 'tests/src/loops.rs', lines 366:0-366:59 *)
 Definition ignore_input_shared_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
   _ <- ignore_input_shared_borrow_loop n i; Ok _a