Update output files

1 files changed, 49 insertions, 49 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index bc8708f4..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 7:0-17: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 7:0-7: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 22:0-34: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 22:0-22: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 37:0-51: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 37:0-37: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 53:0-61: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 53:0-53: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 65:0-71: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 65:0-65: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 73:0-73: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 79:0-88: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 79:0-79: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 91:0-101: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 91:0-91: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 104:0-114: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 104:0-104: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 116:0-130: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 116:0-116: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 132:0-146: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 132:0-132: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 148:0-148: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 152:0-152: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 157:0-168: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 157:0-157: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 171:0-182: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 171:0-171: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 187:0-208: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 187:0-191: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 211:0-232: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 211:0-215: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 236:0-251: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 236:0-240: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 254:0-269: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 254:0-258: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 272:0-287: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 272:0-276: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 291:0-306: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 291:0-295: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 310:0-325: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 310:0-314: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 329:0-344: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 329:0-333: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 348:0-352: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 348:0-348: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 356:0-361: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 356:0-356: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 365:0-369: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 365:0-365: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