From 49117ba254679f98938223711810191c3f7d788f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 27 Oct 2023 13:34:03 +0200
Subject: Regenerate the Coq test files

---
 tests/coq/misc/Loops.v | 412 +++++++++++++++++++++++++------------------------
 1 file changed, 212 insertions(+), 200 deletions(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 82e57576..180a1d68 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -9,23 +9,23 @@ Local Open Scope Primitives_scope.
 Module Loops.
 
 (** [loops::sum]: loop 0: forward function *)
-Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
+Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     if i s< max
-    then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop_fwd n0 max i0 s0)
+    then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop n0 max i0 s0)
     else u32_mul s 2%u32
   end
 .
 
 (** [loops::sum]: forward function *)
-Definition sum_fwd (n : nat) (max : u32) : result u32 :=
-  sum_loop_fwd n max 0%u32 0%u32
+Definition sum (n : nat) (max : u32) : result u32 :=
+  sum_loop n max 0%u32 0%u32
 .
 
 (** [loops::sum_with_mut_borrows]: loop 0: forward function *)
-Fixpoint sum_with_mut_borrows_loop_fwd
+Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -34,18 +34,18 @@ Fixpoint sum_with_mut_borrows_loop_fwd
     then (
       ms0 <- u32_add ms mi;
       mi0 <- u32_add mi 1%u32;
-      sum_with_mut_borrows_loop_fwd n0 max mi0 ms0)
+      sum_with_mut_borrows_loop n0 max mi0 ms0)
     else u32_mul ms 2%u32
   end
 .
 
 (** [loops::sum_with_mut_borrows]: forward function *)
-Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 :=
-  sum_with_mut_borrows_loop_fwd n max 0%u32 0%u32
+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: forward function *)
-Fixpoint sum_with_shared_borrows_loop_fwd
+Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -54,87 +54,88 @@ Fixpoint sum_with_shared_borrows_loop_fwd
     then (
       i0 <- u32_add i 1%u32;
       s0 <- u32_add s i0;
-      sum_with_shared_borrows_loop_fwd n0 max i0 s0)
+      sum_with_shared_borrows_loop n0 max i0 s0)
     else u32_mul s 2%u32
   end
 .
 
 (** [loops::sum_with_shared_borrows]: forward function *)
-Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
-  sum_with_shared_borrows_loop_fwd n max 0%u32 0%u32
+Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
+  sum_with_shared_borrows_loop n max 0%u32 0%u32
 .
 
 (** [loops::clear]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
-Fixpoint clear_loop_fwd_back
-  (n : nat) (v : vec u32) (i : usize) : result (vec u32) :=
+Fixpoint clear_loop
+  (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len u32 v in
+    let i0 := alloc_vec_Vec_len u32 v in
     if i s< i0
     then (
       i1 <- usize_add i 1%usize;
-      v0 <- vec_index_mut_back u32 v i 0%u32;
-      clear_loop_fwd_back n0 v0 i1)
+      v0 <-
+        alloc_vec_Vec_index_mut_back u32 usize
+          (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0%u32;
+      clear_loop n0 v0 i1)
     else Return v
   end
 .
 
 (** [loops::clear]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
-Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) :=
-  clear_loop_fwd_back n v 0%usize
+Definition clear
+  (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) :=
+  clear_loop n v 0%usize
 .
 
 (** [loops::List] *)
 Inductive List_t (T : Type) :=
-| ListCons : T -> List_t T -> List_t T
-| ListNil : List_t T
+| List_Cons : T -> List_t T -> List_t T
+| List_Nil : List_t T
 .
 
-Arguments ListCons {T} _ _.
-Arguments ListNil {T}.
+Arguments List_Cons {T} _ _.
+Arguments List_Nil {T}.
 
 (** [loops::list_mem]: loop 0: forward function *)
-Fixpoint list_mem_loop_fwd
-  (n : nat) (x : u32) (ls : List_t u32) : result bool :=
+Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons y tl =>
-      if y s= x then Return true else list_mem_loop_fwd n0 x tl
-    | ListNil => Return false
+    | List_Cons y tl => if y s= x then Return true else list_mem_loop n0 x tl
+    | List_Nil => Return false
     end
   end
 .
 
 (** [loops::list_mem]: forward function *)
-Definition list_mem_fwd (n : nat) (x : u32) (ls : List_t u32) : result bool :=
-  list_mem_loop_fwd n x ls
+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: forward function *)
-Fixpoint list_nth_mut_loop_loop_fwd
+Fixpoint list_nth_mut_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
       then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop_fwd T n0 tl i0)
-    | ListNil => Fail_ Failure
+      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop T n0 tl i0)
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_loop]: forward function *)
-Definition list_nth_mut_loop_fwd
+Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  list_nth_mut_loop_loop_fwd T n ls i
+  list_nth_mut_loop_loop T n ls i
 .
 
 (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
@@ -146,14 +147,14 @@ Fixpoint list_nth_mut_loop_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
-      then Return (ListCons ret tl)
+      then Return (List_Cons ret tl)
       else (
         i0 <- u32_sub i 1%u32;
         tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
-        Return (ListCons x tl0))
-    | ListNil => Fail_ Failure
+        Return (List_Cons x tl0))
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -167,46 +168,50 @@ Definition list_nth_mut_loop_back
 .
 
 (** [loops::list_nth_shared_loop]: loop 0: forward function *)
-Fixpoint list_nth_shared_loop_loop_fwd
+Fixpoint list_nth_shared_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
       then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop_fwd T n0 tl i0)
-    | ListNil => Fail_ Failure
+      else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n0 tl i0)
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_loop]: forward function *)
-Definition list_nth_shared_loop_fwd
+Definition list_nth_shared_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  list_nth_shared_loop_loop_fwd T n ls i
+  list_nth_shared_loop_loop T n ls i
 .
 
 (** [loops::get_elem_mut]: loop 0: forward function *)
-Fixpoint get_elem_mut_loop_fwd
+Fixpoint get_elem_mut_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons y tl =>
-      if y s= x then Return y else get_elem_mut_loop_fwd n0 x tl
-    | ListNil => Fail_ Failure
+    | List_Cons y tl => if y s= x then Return y else get_elem_mut_loop n0 x tl
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::get_elem_mut]: forward function *)
-Definition get_elem_mut_fwd
-  (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
-  l <- vec_index_mut_fwd (List_t usize) slots 0%usize;
-  get_elem_mut_loop_fwd n x l
+Definition get_elem_mut
+  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
+  result usize
+  :=
+  l <-
+    alloc_vec_Vec_index_mut (List_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
+      slots 0%usize;
+  get_elem_mut_loop n x l
 .
 
 (** [loops::get_elem_mut]: loop 0: backward function 0 *)
@@ -218,50 +223,60 @@ Fixpoint get_elem_mut_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons y tl =>
+    | List_Cons y tl =>
       if y s= x
-      then Return (ListCons ret tl)
-      else (tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y tl0))
-    | ListNil => Fail_ Failure
+      then Return (List_Cons ret tl)
+      else (
+        tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (List_Cons y tl0))
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::get_elem_mut]: backward function 0 *)
 Definition get_elem_mut_back
-  (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) :
-  result (vec (List_t usize))
+  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) (ret : usize) :
+  result (alloc_vec_Vec (List_t usize))
   :=
-  l <- vec_index_mut_fwd (List_t usize) slots 0%usize;
+  l <-
+    alloc_vec_Vec_index_mut (List_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
+      slots 0%usize;
   l0 <- get_elem_mut_loop_back n x l ret;
-  vec_index_mut_back (List_t usize) slots 0%usize l0
+  alloc_vec_Vec_index_mut_back (List_t usize) usize
+    (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) slots
+    0%usize l0
 .
 
 (** [loops::get_elem_shared]: loop 0: forward function *)
-Fixpoint get_elem_shared_loop_fwd
+Fixpoint get_elem_shared_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons y tl =>
-      if y s= x then Return y else get_elem_shared_loop_fwd n0 x tl
-    | ListNil => Fail_ Failure
+    | List_Cons y tl =>
+      if y s= x then Return y else get_elem_shared_loop n0 x tl
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::get_elem_shared]: forward function *)
-Definition get_elem_shared_fwd
-  (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
-  l <- vec_index_fwd (List_t usize) slots 0%usize;
-  get_elem_shared_loop_fwd n x l
+Definition get_elem_shared
+  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
+  result usize
+  :=
+  l <-
+    alloc_vec_Vec_index (List_t usize) usize
+      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
+      slots 0%usize;
+  get_elem_shared_loop n x l
 .
 
 (** [loops::id_mut]: forward function *)
-Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
-  Return ls
-.
+Definition id_mut (T : Type) (ls : List_t T) : result (List_t T) :=
+  Return ls.
 
 (** [loops::id_mut]: backward function 0 *)
 Definition id_mut_back
@@ -270,31 +285,30 @@ Definition id_mut_back
 .
 
 (** [loops::id_shared]: forward function *)
-Definition id_shared_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
+Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
 .
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
-Fixpoint list_nth_mut_loop_with_id_loop_fwd
+Fixpoint list_nth_mut_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
       then Return x
-      else (
-        i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop_fwd T n0 i0 tl)
-    | ListNil => Fail_ Failure
+      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop T n0 i0 tl)
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_loop_with_id]: forward function *)
-Definition list_nth_mut_loop_with_id_fwd
+Definition list_nth_mut_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  ls0 <- id_mut_fwd T ls; list_nth_mut_loop_with_id_loop_fwd T n i ls0
+  ls0 <- id_mut T ls; list_nth_mut_loop_with_id_loop T n i ls0
 .
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
@@ -306,14 +320,14 @@ Fixpoint list_nth_mut_loop_with_id_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
-      then Return (ListCons ret tl)
+      then Return (List_Cons ret tl)
       else (
         i0 <- u32_sub i 1%u32;
         tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
-        Return (ListCons x tl0))
-    | ListNil => Fail_ Failure
+        Return (List_Cons x tl0))
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -323,36 +337,36 @@ Definition list_nth_mut_loop_with_id_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
-  ls0 <- id_mut_fwd T ls;
+  ls0 <- id_mut T ls;
   l <- list_nth_mut_loop_with_id_loop_back T n i ls0 ret;
   id_mut_back T ls l
 .
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
-Fixpoint list_nth_shared_loop_with_id_loop_fwd
+Fixpoint list_nth_shared_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons x tl =>
+    | List_Cons x tl =>
       if i s= 0%u32
       then Return x
       else (
-        i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop_fwd T n0 i0 tl)
-    | ListNil => Fail_ Failure
+        i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n0 i0 tl)
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_loop_with_id]: forward function *)
-Definition list_nth_shared_loop_with_id_fwd
+Definition list_nth_shared_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n i ls0
+  ls0 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls0
 .
 
 (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
-Fixpoint list_nth_mut_loop_pair_loop_fwd
+Fixpoint list_nth_mut_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
@@ -360,27 +374,26 @@ Fixpoint list_nth_mut_loop_pair_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          i0 <- u32_sub i 1%u32; list_nth_mut_loop_pair_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_loop_pair]: forward function *)
-Definition list_nth_mut_loop_pair_fwd
+Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_mut_loop_pair_loop_fwd T n ls0 ls1 i
+  list_nth_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
@@ -392,18 +405,18 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl0)
+        then Return (List_Cons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
           tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x0 tl00))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -425,18 +438,18 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl1)
+        then Return (List_Cons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
           tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x1 tl10))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -450,7 +463,7 @@ Definition list_nth_mut_loop_pair_back'b
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
-Fixpoint list_nth_shared_loop_pair_loop_fwd
+Fixpoint list_nth_shared_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
@@ -458,31 +471,30 @@ Fixpoint list_nth_shared_loop_pair_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          i0 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_loop_pair]: forward function *)
-Definition list_nth_shared_loop_pair_fwd
+Definition list_nth_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i
+  list_nth_shared_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
-Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
+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)
   :=
@@ -490,27 +502,27 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_mut_loop_pair_merge_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]: forward function *)
-Definition list_nth_mut_loop_pair_merge_fwd
+Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
+  list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
@@ -523,19 +535,19 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1)
+        then let (t, t0) := ret in Return (List_Cons t tl0, List_Cons t0 tl1)
         else (
           i0 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
           let (tl00, tl10) := p in
-          Return (ListCons x0 tl00, ListCons x1 tl10))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x0 tl00, List_Cons x1 tl10))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -550,7 +562,7 @@ Definition list_nth_mut_loop_pair_merge_back
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
-Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
+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)
   :=
@@ -558,31 +570,31 @@ Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_shared_loop_pair_merge_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: forward function *)
-Definition list_nth_shared_loop_pair_merge_fwd
+Definition list_nth_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+  list_nth_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
-Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
+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)
   :=
@@ -590,27 +602,27 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_mut_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_mut_shared_loop_pair_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]: forward function *)
-Definition list_nth_mut_shared_loop_pair_fwd
+Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i
+  list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
@@ -622,18 +634,18 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl0)
+        then Return (List_Cons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
           tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x0 tl00))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -647,7 +659,7 @@ Definition list_nth_mut_shared_loop_pair_back
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
-Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
+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)
   :=
@@ -655,27 +667,27 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_mut_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_mut_shared_loop_pair_merge_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
-Definition list_nth_mut_shared_loop_pair_merge_fwd
+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)
   :=
-  list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+  list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
@@ -687,19 +699,19 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl0)
+        then Return (List_Cons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
           tl00 <-
             list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x0 tl00))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -713,7 +725,7 @@ Definition list_nth_mut_shared_loop_pair_merge_back
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
-Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
+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)
   :=
@@ -721,27 +733,27 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_shared_mut_loop_pair_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: forward function *)
-Definition list_nth_shared_mut_loop_pair_fwd
+Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
-  list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i
+  list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
@@ -753,18 +765,18 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl1)
+        then Return (List_Cons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
           tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x1 tl10))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
@@ -778,7 +790,7 @@ Definition list_nth_shared_mut_loop_pair_back
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
-Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
+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)
   :=
@@ -786,27 +798,27 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
         else (
           i0 <- u32_sub i 1%u32;
-          list_nth_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
-      | ListNil => Fail_ Failure
+          list_nth_shared_mut_loop_pair_merge_loop T n0 tl0 tl1 i0)
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
-Definition list_nth_shared_mut_loop_pair_merge_fwd
+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)
   :=
-  list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
+  list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
@@ -818,19 +830,19 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls0 with
-    | ListCons x0 tl0 =>
+    | List_Cons x0 tl0 =>
       match ls1 with
-      | ListCons x1 tl1 =>
+      | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (ListCons ret tl1)
+        then Return (List_Cons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
           tl10 <-
             list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10))
-      | ListNil => Fail_ Failure
+          Return (List_Cons x1 tl10))
+      | List_Nil => Fail_ Failure
       end
-    | ListNil => Fail_ Failure
+    | List_Nil => Fail_ Failure
     end
   end
 .
-- 
cgit v1.2.3


From 49ffc966cfdbd71f8c83a3c72ab81e1bb101f420 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 16:24:07 +0100
Subject: Regenerate the Coq test files

---
 tests/coq/misc/Loops.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 180a1d68..1c0eab17 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -96,8 +96,8 @@ Inductive List_t (T : Type) :=
 | List_Nil : List_t T
 .
 
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
 
 (** [loops::list_mem]: loop 0: forward function *)
 Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
-- 
cgit v1.2.3


From 5e92ae6b361f9221f5c5f9a39ab4c28a36597a77 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 11:40:59 +0100
Subject: Regenerate most of the test files

---
 tests/coq/misc/Loops.v | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 1c0eab17..e5ff6c8e 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -77,7 +77,7 @@ Fixpoint clear_loop
       i1 <- usize_add i 1%usize;
       v0 <-
         alloc_vec_Vec_index_mut_back u32 usize
-          (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0%u32;
+          (core_slice_index_SliceIndexUsizeSliceTInst u32) v i 0%u32;
       clear_loop n0 v0 i1)
     else Return v
   end
@@ -209,8 +209,7 @@ Definition get_elem_mut
   :=
   l <-
     alloc_vec_Vec_index_mut (List_t usize) usize
-      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
-      slots 0%usize;
+      (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
   get_elem_mut_loop n x l
 .
 
@@ -240,12 +239,11 @@ Definition get_elem_mut_back
   :=
   l <-
     alloc_vec_Vec_index_mut (List_t usize) usize
-      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
-      slots 0%usize;
+      (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
   l0 <- get_elem_mut_loop_back n x l ret;
   alloc_vec_Vec_index_mut_back (List_t usize) usize
-    (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) slots
-    0%usize l0
+    (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize
+    l0
 .
 
 (** [loops::get_elem_shared]: loop 0: forward function *)
@@ -269,8 +267,7 @@ Definition get_elem_shared
   :=
   l <-
     alloc_vec_Vec_index (List_t usize) usize
-      (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize))
-      slots 0%usize;
+      (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
   get_elem_shared_loop n x l
 .
 
-- 
cgit v1.2.3


From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:57:38 +0100
Subject: Regenerate the files

---
 tests/coq/misc/Loops.v | 186 ++++++++++++++++++++++++++++++++-----------------
 1 file changed, 124 insertions(+), 62 deletions(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e5ff6c8e..4929ddd0 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -8,7 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Loops.
 
-(** [loops::sum]: loop 0: forward function *)
+(** [loops::sum]: loop 0: forward function
+    Source: 'src/loops.rs', lines 4:0-14:1 *)
 Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -19,12 +20,14 @@ Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   end
 .
 
-(** [loops::sum]: forward function *)
+(** [loops::sum]: forward function
+    Source: 'src/loops.rs', lines 4:0-4:27 *)
 Definition sum (n : nat) (max : u32) : result u32 :=
   sum_loop n max 0%u32 0%u32
 .
 
-(** [loops::sum_with_mut_borrows]: loop 0: forward function *)
+(** [loops::sum_with_mut_borrows]: loop 0: forward function
+    Source: 'src/loops.rs', lines 19:0-31:1 *)
 Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
   match n with
@@ -39,12 +42,14 @@ Fixpoint sum_with_mut_borrows_loop
   end
 .
 
-(** [loops::sum_with_mut_borrows]: forward function *)
+(** [loops::sum_with_mut_borrows]: forward function
+    Source: 'src/loops.rs', lines 19:0-19: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: forward function *)
+(** [loops::sum_with_shared_borrows]: loop 0: forward function
+    Source: 'src/loops.rs', lines 34:0-48:1 *)
 Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -59,13 +64,15 @@ Fixpoint sum_with_shared_borrows_loop
   end
 .
 
-(** [loops::sum_with_shared_borrows]: forward function *)
+(** [loops::sum_with_shared_borrows]: forward function
+    Source: 'src/loops.rs', lines 34:0-34:47 *)
 Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
   sum_with_shared_borrows_loop n max 0%u32 0%u32
 .
 
 (** [loops::clear]: loop 0: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/loops.rs', lines 52:0-58:1 *)
 Fixpoint clear_loop
   (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with
@@ -84,13 +91,15 @@ Fixpoint clear_loop
 .
 
 (** [loops::clear]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/loops.rs', lines 52:0-52:30 *)
 Definition clear
   (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) :=
   clear_loop n v 0%usize
 .
 
-(** [loops::List] *)
+(** [loops::List]
+    Source: 'src/loops.rs', lines 60:0-60:16 *)
 Inductive List_t (T : Type) :=
 | List_Cons : T -> List_t T -> List_t T
 | List_Nil : List_t T
@@ -99,7 +108,8 @@ Inductive List_t (T : Type) :=
 Arguments List_Cons { _ }.
 Arguments List_Nil { _ }.
 
-(** [loops::list_mem]: loop 0: forward function *)
+(** [loops::list_mem]: loop 0: forward function
+    Source: 'src/loops.rs', lines 66:0-75:1 *)
 Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
@@ -111,12 +121,14 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   end
 .
 
-(** [loops::list_mem]: forward function *)
+(** [loops::list_mem]: forward function
+    Source: 'src/loops.rs', lines 66:0-66: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: forward function *)
+(** [loops::list_nth_mut_loop]: loop 0: forward function
+    Source: 'src/loops.rs', lines 78:0-88:1 *)
 Fixpoint list_nth_mut_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -132,13 +144,15 @@ Fixpoint list_nth_mut_loop_loop
   end
 .
 
-(** [loops::list_nth_mut_loop]: forward function *)
+(** [loops::list_nth_mut_loop]: forward function
+    Source: 'src/loops.rs', lines 78:0-78:71 *)
 Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   list_nth_mut_loop_loop T n ls i
 .
 
-(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_loop]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 78:0-88:1 *)
 Fixpoint list_nth_mut_loop_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -159,7 +173,8 @@ Fixpoint list_nth_mut_loop_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop]: backward function 0 *)
+(** [loops::list_nth_mut_loop]: backward function 0
+    Source: 'src/loops.rs', lines 78:0-78:71 *)
 Definition list_nth_mut_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -167,7 +182,8 @@ Definition list_nth_mut_loop_back
   list_nth_mut_loop_loop_back T n ls i ret
 .
 
-(** [loops::list_nth_shared_loop]: loop 0: forward function *)
+(** [loops::list_nth_shared_loop]: loop 0: forward function
+    Source: 'src/loops.rs', lines 91:0-101:1 *)
 Fixpoint list_nth_shared_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -183,13 +199,15 @@ Fixpoint list_nth_shared_loop_loop
   end
 .
 
-(** [loops::list_nth_shared_loop]: forward function *)
+(** [loops::list_nth_shared_loop]: forward function
+    Source: 'src/loops.rs', lines 91:0-91: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: forward function *)
+(** [loops::get_elem_mut]: loop 0: forward function
+    Source: 'src/loops.rs', lines 103:0-117:1 *)
 Fixpoint get_elem_mut_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -202,7 +220,8 @@ Fixpoint get_elem_mut_loop
   end
 .
 
-(** [loops::get_elem_mut]: forward function *)
+(** [loops::get_elem_mut]: forward function
+    Source: 'src/loops.rs', lines 103:0-103:73 *)
 Definition get_elem_mut
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
@@ -213,7 +232,8 @@ Definition get_elem_mut
   get_elem_mut_loop n x l
 .
 
-(** [loops::get_elem_mut]: loop 0: backward function 0 *)
+(** [loops::get_elem_mut]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 103:0-117:1 *)
 Fixpoint get_elem_mut_loop_back
   (n : nat) (x : usize) (ls : List_t usize) (ret : usize) :
   result (List_t usize)
@@ -232,7 +252,8 @@ Fixpoint get_elem_mut_loop_back
   end
 .
 
-(** [loops::get_elem_mut]: backward function 0 *)
+(** [loops::get_elem_mut]: backward function 0
+    Source: 'src/loops.rs', lines 103:0-103:73 *)
 Definition get_elem_mut_back
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) (ret : usize) :
   result (alloc_vec_Vec (List_t usize))
@@ -246,7 +267,8 @@ Definition get_elem_mut_back
     l0
 .
 
-(** [loops::get_elem_shared]: loop 0: forward function *)
+(** [loops::get_elem_shared]: loop 0: forward function
+    Source: 'src/loops.rs', lines 119:0-133:1 *)
 Fixpoint get_elem_shared_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -260,7 +282,8 @@ Fixpoint get_elem_shared_loop
   end
 .
 
-(** [loops::get_elem_shared]: forward function *)
+(** [loops::get_elem_shared]: forward function
+    Source: 'src/loops.rs', lines 119:0-119:68 *)
 Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
@@ -271,22 +294,26 @@ Definition get_elem_shared
   get_elem_shared_loop n x l
 .
 
-(** [loops::id_mut]: forward function *)
+(** [loops::id_mut]: forward function
+    Source: 'src/loops.rs', lines 135:0-135:50 *)
 Definition id_mut (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls.
 
-(** [loops::id_mut]: backward function 0 *)
+(** [loops::id_mut]: backward function 0
+    Source: 'src/loops.rs', lines 135:0-135:50 *)
 Definition id_mut_back
   (T : Type) (ls : List_t T) (ret : List_t T) : result (List_t T) :=
   Return ret
 .
 
-(** [loops::id_shared]: forward function *)
+(** [loops::id_shared]: forward function
+    Source: 'src/loops.rs', lines 139:0-139:45 *)
 Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
 .
 
-(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
+(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function
+    Source: 'src/loops.rs', lines 144:0-155:1 *)
 Fixpoint list_nth_mut_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -302,13 +329,15 @@ Fixpoint list_nth_mut_loop_with_id_loop
   end
 .
 
-(** [loops::list_nth_mut_loop_with_id]: forward function *)
+(** [loops::list_nth_mut_loop_with_id]: forward function
+    Source: 'src/loops.rs', lines 144:0-144:75 *)
 Definition list_nth_mut_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   ls0 <- id_mut T ls; list_nth_mut_loop_with_id_loop T n i ls0
 .
 
-(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 144:0-155:1 *)
 Fixpoint list_nth_mut_loop_with_id_loop_back
   (T : Type) (n : nat) (i : u32) (ls : List_t T) (ret : T) :
   result (List_t T)
@@ -329,7 +358,8 @@ Fixpoint list_nth_mut_loop_with_id_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
+(** [loops::list_nth_mut_loop_with_id]: backward function 0
+    Source: 'src/loops.rs', lines 144:0-144:75 *)
 Definition list_nth_mut_loop_with_id_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -339,7 +369,8 @@ Definition list_nth_mut_loop_with_id_back
   id_mut_back T ls l
 .
 
-(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
+(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function
+    Source: 'src/loops.rs', lines 158:0-169:1 *)
 Fixpoint list_nth_shared_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -356,13 +387,15 @@ Fixpoint list_nth_shared_loop_with_id_loop
   end
 .
 
-(** [loops::list_nth_shared_loop_with_id]: forward function *)
+(** [loops::list_nth_shared_loop_with_id]: forward function
+    Source: 'src/loops.rs', lines 158:0-158:70 *)
 Definition list_nth_shared_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   ls0 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls0
 .
 
-(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: forward function
+    Source: 'src/loops.rs', lines 174:0-195: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)
@@ -385,7 +418,8 @@ Fixpoint list_nth_mut_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_mut_loop_pair]: forward function *)
+(** [loops::list_nth_mut_loop_pair]: forward function
+    Source: 'src/loops.rs', lines 174:0-178:27 *)
 Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -393,7 +427,8 @@ Definition list_nth_mut_loop_pair
   list_nth_mut_loop_pair_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 174:0-195:1 *)
 Fixpoint list_nth_mut_loop_pair_loop_back'a
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -418,7 +453,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a
   end
 .
 
-(** [loops::list_nth_mut_loop_pair]: backward function 0 *)
+(** [loops::list_nth_mut_loop_pair]: backward function 0
+    Source: 'src/loops.rs', lines 174:0-178:27 *)
 Definition list_nth_mut_loop_pair_back'a
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -426,7 +462,8 @@ Definition list_nth_mut_loop_pair_back'a
   list_nth_mut_loop_pair_loop_back'a T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1
+    Source: 'src/loops.rs', lines 174:0-195:1 *)
 Fixpoint list_nth_mut_loop_pair_loop_back'b
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -451,7 +488,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b
   end
 .
 
-(** [loops::list_nth_mut_loop_pair]: backward function 1 *)
+(** [loops::list_nth_mut_loop_pair]: backward function 1
+    Source: 'src/loops.rs', lines 174:0-178:27 *)
 Definition list_nth_mut_loop_pair_back'b
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -459,7 +497,8 @@ Definition list_nth_mut_loop_pair_back'b
   list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
+(** [loops::list_nth_shared_loop_pair]: loop 0: forward function
+    Source: 'src/loops.rs', lines 198:0-219: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)
@@ -482,7 +521,8 @@ Fixpoint list_nth_shared_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_shared_loop_pair]: forward function *)
+(** [loops::list_nth_shared_loop_pair]: forward function
+    Source: 'src/loops.rs', lines 198:0-202:19 *)
 Definition list_nth_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -490,7 +530,8 @@ Definition list_nth_shared_loop_pair
   list_nth_shared_loop_pair_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function
+    Source: 'src/loops.rs', lines 223:0-238: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)
@@ -514,7 +555,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: forward function *)
+(** [loops::list_nth_mut_loop_pair_merge]: forward function
+    Source: 'src/loops.rs', lines 223:0-227: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)
@@ -522,7 +564,8 @@ Definition list_nth_mut_loop_pair_merge
   list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 223:0-238:1 *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
   (ret : (T * T)) :
@@ -549,7 +592,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
+(** [loops::list_nth_mut_loop_pair_merge]: backward function 0
+    Source: 'src/loops.rs', lines 223:0-227:27 *)
 Definition list_nth_mut_loop_pair_merge_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
   (ret : (T * T)) :
@@ -558,7 +602,8 @@ Definition list_nth_mut_loop_pair_merge_back
   list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
+(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function
+    Source: 'src/loops.rs', lines 241:0-256: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)
@@ -582,7 +627,8 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_shared_loop_pair_merge]: forward function *)
+(** [loops::list_nth_shared_loop_pair_merge]: forward function
+    Source: 'src/loops.rs', lines 241:0-245: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)
@@ -590,7 +636,8 @@ Definition list_nth_shared_loop_pair_merge
   list_nth_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function
+    Source: 'src/loops.rs', lines 259:0-274: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)
@@ -614,7 +661,8 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: forward function *)
+(** [loops::list_nth_mut_shared_loop_pair]: forward function
+    Source: 'src/loops.rs', lines 259:0-263: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)
@@ -622,7 +670,8 @@ Definition list_nth_mut_shared_loop_pair
   list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 259:0-274:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -647,7 +696,8 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
+(** [loops::list_nth_mut_shared_loop_pair]: backward function 0
+    Source: 'src/loops.rs', lines 259:0-263:23 *)
 Definition list_nth_mut_shared_loop_pair_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -655,7 +705,8 @@ Definition list_nth_mut_shared_loop_pair_back
   list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function
+    Source: 'src/loops.rs', lines 278:0-293: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)
@@ -679,7 +730,8 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function
+    Source: 'src/loops.rs', lines 278:0-282: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)
@@ -687,7 +739,8 @@ Definition list_nth_mut_shared_loop_pair_merge
   list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 278:0-293:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -713,7 +766,8 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0
+    Source: 'src/loops.rs', lines 278:0-282:23 *)
 Definition list_nth_mut_shared_loop_pair_merge_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -721,7 +775,8 @@ Definition list_nth_mut_shared_loop_pair_merge_back
   list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function
+    Source: 'src/loops.rs', lines 297:0-312: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)
@@ -745,7 +800,8 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: forward function *)
+(** [loops::list_nth_shared_mut_loop_pair]: forward function
+    Source: 'src/loops.rs', lines 297:0-301: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)
@@ -753,7 +809,8 @@ Definition list_nth_shared_mut_loop_pair
   list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1
+    Source: 'src/loops.rs', lines 297:0-312:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -778,7 +835,8 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
+(** [loops::list_nth_shared_mut_loop_pair]: backward function 1
+    Source: 'src/loops.rs', lines 297:0-301:23 *)
 Definition list_nth_shared_mut_loop_pair_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -786,7 +844,8 @@ Definition list_nth_shared_mut_loop_pair_back
   list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function
+    Source: 'src/loops.rs', lines 316:0-331: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)
@@ -810,7 +869,8 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function
+    Source: 'src/loops.rs', lines 316:0-320: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)
@@ -818,7 +878,8 @@ Definition list_nth_shared_mut_loop_pair_merge
   list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0
+    Source: 'src/loops.rs', lines 316:0-331:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -844,7 +905,8 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0
+    Source: 'src/loops.rs', lines 316:0-320:23 *)
 Definition list_nth_shared_mut_loop_pair_merge_back
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
-- 
cgit v1.2.3


From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types

---
 tests/coq/misc/Loops.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4929ddd0..83c249c1 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -914,4 +914,4 @@ Definition list_nth_shared_mut_loop_pair_merge_back
   list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-End Loops .
+End Loops.
-- 
cgit v1.2.3