From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 12:20:28 +0200
Subject: Improve the generated comments

---
 tests/coq/misc/Constants.v       |  16 ++---
 tests/coq/misc/External_Funs.v   |  18 +++---
 tests/coq/misc/External_Opaque.v |  10 ++--
 tests/coq/misc/Loops.v           | 124 ++++++++++++++++++++-------------------
 tests/coq/misc/NoNestedBorrows.v | 112 ++++++++++++++++++-----------------
 tests/coq/misc/Paper.v           |  21 +++----
 tests/coq/misc/PoloniusList.v    |   4 +-
 tests/coq/misc/_CoqProject       |   6 +-
 8 files changed, 158 insertions(+), 153 deletions(-)

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 6a5f2696..14c05c61 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -22,7 +22,7 @@ Definition x1_c : u32 := x1_body%global.
 Definition x2_body : result u32 := Return 3%u32.
 Definition x2_c : u32 := x2_body%global.
 
-(** [constants::incr] *)
+(** [constants::incr]: forward function *)
 Definition incr_fwd (n : u32) : result u32 :=
   u32_add n 1%u32.
 
@@ -30,7 +30,7 @@ Definition incr_fwd (n : u32) : result u32 :=
 Definition x3_body : result u32 := incr_fwd 32%u32.
 Definition x3_c : u32 := x3_body%global.
 
-(** [constants::mk_pair0] *)
+(** [constants::mk_pair0]: forward function *)
 Definition mk_pair0_fwd (x : u32) (y : u32) : result (u32 * u32) :=
   Return (x, y)
 .
@@ -42,7 +42,7 @@ Arguments mkPair_t {T1} {T2} _ _.
 Arguments Pair_x {T1} {T2}.
 Arguments Pair_y {T1} {T2}.
 
-(** [constants::mk_pair1] *)
+(** [constants::mk_pair1]: forward function *)
 Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
   Return {| Pair_x := x; Pair_y := y |}
 .
@@ -71,7 +71,7 @@ Record Wrap_t (T : Type) := mkWrap_t { Wrap_val : T; }.
 Arguments mkWrap_t {T} _.
 Arguments Wrap_val {T}.
 
-(** [constants::Wrap::{0}::new] *)
+(** [constants::Wrap::{0}::new]: forward function *)
 Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
   Return {| Wrap_val := val |}
 .
@@ -80,7 +80,7 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
 Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 2%i32.
 Definition y_c : Wrap_t i32 := y_body%global.
 
-(** [constants::unwrap_y] *)
+(** [constants::unwrap_y]: forward function *)
 Definition unwrap_y_fwd : result i32 :=
   Return y_c.(Wrap_val).
 
@@ -92,11 +92,11 @@ Definition yval_c : i32 := yval_body%global.
 Definition get_z1_z1_body : result i32 := Return 3%i32.
 Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
 
-(** [constants::get_z1] *)
+(** [constants::get_z1]: forward function *)
 Definition get_z1_fwd : result i32 :=
   Return get_z1_z1_c.
 
-(** [constants::add] *)
+(** [constants::add]: forward function *)
 Definition add_fwd (a : i32) (b : i32) : result i32 :=
   i32_add a b.
 
@@ -112,7 +112,7 @@ Definition q2_c : i32 := q2_body%global.
 Definition q3_body : result i32 := add_fwd q2_c 3%i32.
 Definition q3_c : i32 := q3_body%global.
 
-(** [constants::get_z2] *)
+(** [constants::get_z2]: forward function *)
 Definition get_z2_fwd : result i32 :=
   i <- get_z1_fwd; i0 <- add_fwd i q3_c; add_fwd q1_c i0
 .
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 05dd8f2e..f18bbd1f 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -10,7 +10,7 @@ Require Export External_Opaque.
 Import External_Opaque.
 Module External_Funs.
 
-(** [external::swap] *)
+(** [external::swap]: forward function *)
 Definition swap_fwd
   (T : Type) (x : T) (y : T) (st : state) : result (state * unit) :=
   p <- core_mem_swap_fwd T x y st;
@@ -22,7 +22,7 @@ Definition swap_fwd
   Return (st2, tt)
 .
 
-(** [external::swap] *)
+(** [external::swap]: backward function 0 *)
 Definition swap_back
   (T : Type) (x : T) (y : T) (st : state) (st0 : state) :
   result (state * (T * T))
@@ -36,7 +36,7 @@ Definition swap_back
   Return (st0, (x0, y0))
 .
 
-(** [external::test_new_non_zero_u32] *)
+(** [external::test_new_non_zero_u32]: forward function *)
 Definition test_new_non_zero_u32_fwd
   (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) :=
   p <- core_num_nonzero_non_zero_u32_new_fwd x st;
@@ -44,7 +44,7 @@ Definition test_new_non_zero_u32_fwd
   core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0
 .
 
-(** [external::test_vec] *)
+(** [external::test_vec]: forward function *)
 Definition test_vec_fwd : result unit :=
   let v := vec_new u32 in _ <- vec_push_back u32 v 0%u32; Return tt
 .
@@ -52,7 +52,7 @@ Definition test_vec_fwd : result unit :=
 (** Unit test for [external::test_vec] *)
 Check (test_vec_fwd )%return.
 
-(** [external::custom_swap] *)
+(** [external::custom_swap]: forward function *)
 Definition custom_swap_fwd
   (T : Type) (x : T) (y : T) (st : state) : result (state * T) :=
   p <- core_mem_swap_fwd T x y st;
@@ -64,7 +64,7 @@ Definition custom_swap_fwd
   Return (st2, x0)
 .
 
-(** [external::custom_swap] *)
+(** [external::custom_swap]: backward function 0 *)
 Definition custom_swap_back
   (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) :
   result (state * (T * T))
@@ -78,13 +78,13 @@ Definition custom_swap_back
   Return (st0, (ret, y0))
 .
 
-(** [external::test_custom_swap] *)
+(** [external::test_custom_swap]: forward function *)
 Definition test_custom_swap_fwd
   (x : u32) (y : u32) (st : state) : result (state * unit) :=
   p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt)
 .
 
-(** [external::test_custom_swap] *)
+(** [external::test_custom_swap]: backward function 0 *)
 Definition test_custom_swap_back
   (x : u32) (y : u32) (st : state) (st0 : state) :
   result (state * (u32 * u32))
@@ -92,7 +92,7 @@ Definition test_custom_swap_back
   custom_swap_back u32 x y st 1%u32 st0
 .
 
-(** [external::test_swap_non_zero] *)
+(** [external::test_swap_non_zero]: forward function *)
 Definition test_swap_non_zero_fwd
   (x : u32) (st : state) : result (state * u32) :=
   p <- swap_fwd u32 x 0%u32 st;
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
index 5ee65277..1224f426 100644
--- a/tests/coq/misc/External_Opaque.v
+++ b/tests/coq/misc/External_Opaque.v
@@ -8,27 +8,27 @@ Require Export External_Types.
 Import External_Types.
 Module External_Opaque.
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: forward function *)
 Axiom core_mem_swap_fwd :
   forall(T : Type), T -> T -> state -> result (state * unit)
 .
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: backward function 0 *)
 Axiom core_mem_swap_back0 :
   forall(T : Type), T -> T -> state -> state -> result (state * T)
 .
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: backward function 1 *)
 Axiom core_mem_swap_back1 :
   forall(T : Type), T -> T -> state -> state -> result (state * T)
 .
 
-(** [core::num::nonzero::NonZeroU32::{14}::new] *)
+(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *)
 Axiom core_num_nonzero_non_zero_u32_new_fwd
   : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t))
 .
 
-(** [core::option::Option::{0}::unwrap] *)
+(** [core::option::Option::{0}::unwrap]: forward function *)
 Axiom core_option_option_unwrap_fwd :
   forall(T : Type), option T -> state -> result (state * T)
 .
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index a5cb3688..f17eb986 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -6,7 +6,7 @@ Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
 Module Loops.
 
-(** [loops::sum] *)
+(** [loops::sum]: loop 0: forward function *)
 Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -17,12 +17,12 @@ Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   end
 .
 
-(** [loops::sum] *)
+(** [loops::sum]: forward function *)
 Definition sum_fwd (n : nat) (max : u32) : result u32 :=
   sum_loop_fwd n max 0%u32 0%u32
 .
 
-(** [loops::sum_with_mut_borrows] *)
+(** [loops::sum_with_mut_borrows]: loop 0: forward function *)
 Fixpoint sum_with_mut_borrows_loop_fwd
   (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
   match n with
@@ -37,12 +37,12 @@ Fixpoint sum_with_mut_borrows_loop_fwd
   end
 .
 
-(** [loops::sum_with_mut_borrows] *)
+(** [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
 .
 
-(** [loops::sum_with_shared_borrows] *)
+(** [loops::sum_with_shared_borrows]: loop 0: forward function *)
 Fixpoint sum_with_shared_borrows_loop_fwd
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -57,12 +57,13 @@ Fixpoint sum_with_shared_borrows_loop_fwd
   end
 .
 
-(** [loops::sum_with_shared_borrows] *)
+(** [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
 .
 
-(** [loops::clear] *)
+(** [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) :=
   match n with
@@ -78,7 +79,8 @@ Fixpoint clear_loop_fwd_back
   end
 .
 
-(** [loops::clear] *)
+(** [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
 .
@@ -92,7 +94,7 @@ Inductive List_t (T : Type) :=
 Arguments ListCons {T} _ _.
 Arguments ListNil {T}.
 
-(** [loops::list_mem] *)
+(** [loops::list_mem]: loop 0: forward function *)
 Fixpoint list_mem_loop_fwd
   (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
@@ -106,12 +108,12 @@ Fixpoint list_mem_loop_fwd
   end
 .
 
-(** [loops::list_mem] *)
+(** [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
 .
 
-(** [loops::list_nth_mut_loop] *)
+(** [loops::list_nth_mut_loop]: loop 0: forward function *)
 Fixpoint list_nth_mut_loop_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -127,13 +129,13 @@ Fixpoint list_nth_mut_loop_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_loop] *)
+(** [loops::list_nth_mut_loop]: forward function *)
 Definition list_nth_mut_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   list_nth_mut_loop_loop_fwd T n ls i
 .
 
-(** [loops::list_nth_mut_loop] *)
+(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
 Fixpoint list_nth_mut_loop_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -154,7 +156,7 @@ Fixpoint list_nth_mut_loop_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop] *)
+(** [loops::list_nth_mut_loop]: backward function 0 *)
 Definition list_nth_mut_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -162,7 +164,7 @@ Definition list_nth_mut_loop_back
   list_nth_mut_loop_loop_back T n ls i ret
 .
 
-(** [loops::list_nth_shared_loop] *)
+(** [loops::list_nth_shared_loop]: loop 0: forward function *)
 Fixpoint list_nth_shared_loop_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -178,13 +180,13 @@ Fixpoint list_nth_shared_loop_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_loop] *)
+(** [loops::list_nth_shared_loop]: forward function *)
 Definition list_nth_shared_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   list_nth_shared_loop_loop_fwd T n ls i
 .
 
-(** [loops::get_elem_mut] *)
+(** [loops::get_elem_mut]: loop 0: forward function *)
 Fixpoint get_elem_mut_loop_fwd
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -198,14 +200,14 @@ Fixpoint get_elem_mut_loop_fwd
   end
 .
 
-(** [loops::get_elem_mut] *)
+(** [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
 .
 
-(** [loops::get_elem_mut] *)
+(** [loops::get_elem_mut]: loop 0: backward function 0 *)
 Fixpoint get_elem_mut_loop_back
   (n : nat) (x : usize) (ls : List_t usize) (ret : usize) :
   result (List_t usize)
@@ -223,7 +225,7 @@ Fixpoint get_elem_mut_loop_back
   end
 .
 
-(** [loops::get_elem_mut] *)
+(** [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))
@@ -233,7 +235,7 @@ Definition get_elem_mut_back
   vec_index_mut_back (List_t usize) slots 0%usize l0
 .
 
-(** [loops::get_elem_shared] *)
+(** [loops::get_elem_shared]: loop 0: forward function *)
 Fixpoint get_elem_shared_loop_fwd
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -247,30 +249,30 @@ Fixpoint get_elem_shared_loop_fwd
   end
 .
 
-(** [loops::get_elem_shared] *)
+(** [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
 .
 
-(** [loops::id_mut] *)
+(** [loops::id_mut]: forward function *)
 Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
 .
 
-(** [loops::id_mut] *)
+(** [loops::id_mut]: backward function 0 *)
 Definition id_mut_back
   (T : Type) (ls : List_t T) (ret : List_t T) : result (List_t T) :=
   Return ret
 .
 
-(** [loops::id_shared] *)
+(** [loops::id_shared]: forward function *)
 Definition id_shared_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
 .
 
-(** [loops::list_nth_mut_loop_with_id] *)
+(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
 Fixpoint list_nth_mut_loop_with_id_loop_fwd
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -287,13 +289,13 @@ Fixpoint list_nth_mut_loop_with_id_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_loop_with_id] *)
+(** [loops::list_nth_mut_loop_with_id]: forward function *)
 Definition list_nth_mut_loop_with_id_fwd
   (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
 .
 
-(** [loops::list_nth_mut_loop_with_id] *)
+(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
 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)
@@ -314,7 +316,7 @@ Fixpoint list_nth_mut_loop_with_id_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop_with_id] *)
+(** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
 Definition list_nth_mut_loop_with_id_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
@@ -324,7 +326,7 @@ Definition list_nth_mut_loop_with_id_back
   id_mut_back T ls l
 .
 
-(** [loops::list_nth_shared_loop_with_id] *)
+(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
 Fixpoint list_nth_shared_loop_with_id_loop_fwd
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -341,13 +343,13 @@ Fixpoint list_nth_shared_loop_with_id_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_loop_with_id] *)
+(** [loops::list_nth_shared_loop_with_id]: forward function *)
 Definition list_nth_shared_loop_with_id_fwd
   (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
 .
 
-(** [loops::list_nth_mut_loop_pair] *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
 Fixpoint list_nth_mut_loop_pair_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -371,7 +373,7 @@ Fixpoint list_nth_mut_loop_pair_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_loop_pair] *)
+(** [loops::list_nth_mut_loop_pair]: forward function *)
 Definition list_nth_mut_loop_pair_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -379,7 +381,7 @@ Definition list_nth_mut_loop_pair_fwd
   list_nth_mut_loop_pair_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair] *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
 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)
@@ -404,7 +406,7 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a
   end
 .
 
-(** [loops::list_nth_mut_loop_pair] *)
+(** [loops::list_nth_mut_loop_pair]: backward function 0 *)
 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)
@@ -412,7 +414,7 @@ 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] *)
+(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 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)
@@ -437,7 +439,7 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b
   end
 .
 
-(** [loops::list_nth_mut_loop_pair] *)
+(** [loops::list_nth_mut_loop_pair]: backward function 1 *)
 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)
@@ -445,7 +447,7 @@ 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] *)
+(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
 Fixpoint list_nth_shared_loop_pair_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -469,7 +471,7 @@ Fixpoint list_nth_shared_loop_pair_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_loop_pair] *)
+(** [loops::list_nth_shared_loop_pair]: forward function *)
 Definition list_nth_shared_loop_pair_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -477,7 +479,7 @@ Definition list_nth_shared_loop_pair_fwd
   list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair_merge] *)
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -501,7 +503,7 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_loop_pair_merge] *)
+(** [loops::list_nth_mut_loop_pair_merge]: forward function *)
 Definition list_nth_mut_loop_pair_merge_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -509,7 +511,7 @@ Definition list_nth_mut_loop_pair_merge_fwd
   list_nth_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair_merge] *)
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
 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)) :
@@ -536,7 +538,7 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_mut_loop_pair_merge] *)
+(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
 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)) :
@@ -545,7 +547,7 @@ 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] *)
+(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
 Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -569,7 +571,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_loop_pair_merge] *)
+(** [loops::list_nth_shared_loop_pair_merge]: forward function *)
 Definition list_nth_shared_loop_pair_merge_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -577,7 +579,7 @@ Definition list_nth_shared_loop_pair_merge_fwd
   list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair] *)
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -601,7 +603,7 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair] *)
+(** [loops::list_nth_mut_shared_loop_pair]: forward function *)
 Definition list_nth_mut_shared_loop_pair_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -609,7 +611,7 @@ Definition list_nth_mut_shared_loop_pair_fwd
   list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair] *)
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
 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)
@@ -634,7 +636,7 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair] *)
+(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
 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)
@@ -642,7 +644,7 @@ 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] *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -666,7 +668,7 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
 Definition list_nth_mut_shared_loop_pair_merge_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -674,7 +676,7 @@ Definition list_nth_mut_shared_loop_pair_merge_fwd
   list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
 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)
@@ -700,7 +702,7 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
 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)
@@ -708,7 +710,7 @@ 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] *)
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -732,7 +734,7 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair] *)
+(** [loops::list_nth_shared_mut_loop_pair]: forward function *)
 Definition list_nth_shared_mut_loop_pair_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -740,7 +742,7 @@ Definition list_nth_shared_mut_loop_pair_fwd
   list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_shared_mut_loop_pair] *)
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 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)
@@ -765,7 +767,7 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair] *)
+(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
 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)
@@ -773,7 +775,7 @@ 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] *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -797,7 +799,7 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
 Definition list_nth_shared_mut_loop_pair_merge_fwd
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -805,7 +807,7 @@ Definition list_nth_shared_mut_loop_pair_merge_fwd
   list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
 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)
@@ -831,7 +833,7 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
 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)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 96d62711..470a2cde 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -45,47 +45,47 @@ Inductive Sum_t (T1 T2 : Type) :=
 Arguments SumLeft {T1} {T2} _.
 Arguments SumRight {T1} {T2} _.
 
-(** [no_nested_borrows::neg_test] *)
+(** [no_nested_borrows::neg_test]: forward function *)
 Definition neg_test_fwd (x : i32) : result i32 :=
   i32_neg x.
 
-(** [no_nested_borrows::add_test] *)
+(** [no_nested_borrows::add_test]: forward function *)
 Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
   u32_add x y.
 
-(** [no_nested_borrows::subs_test] *)
+(** [no_nested_borrows::subs_test]: forward function *)
 Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
   u32_sub x y.
 
-(** [no_nested_borrows::div_test] *)
+(** [no_nested_borrows::div_test]: forward function *)
 Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
   u32_div x y.
 
-(** [no_nested_borrows::div_test1] *)
+(** [no_nested_borrows::div_test1]: forward function *)
 Definition div_test1_fwd (x : u32) : result u32 :=
   u32_div x 2%u32.
 
-(** [no_nested_borrows::rem_test] *)
+(** [no_nested_borrows::rem_test]: forward function *)
 Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
   u32_rem x y.
 
-(** [no_nested_borrows::cast_test] *)
+(** [no_nested_borrows::cast_test]: forward function *)
 Definition cast_test_fwd (x : u32) : result i32 :=
   scalar_cast U32 I32 x.
 
-(** [no_nested_borrows::test2] *)
+(** [no_nested_borrows::test2]: forward function *)
 Definition test2_fwd : result unit :=
   _ <- u32_add 23%u32 44%u32; Return tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2_fwd )%return.
 
-(** [no_nested_borrows::get_max] *)
+(** [no_nested_borrows::get_max]: forward function *)
 Definition get_max_fwd (x : u32) (y : u32) : result u32 :=
   if x s>= y then Return x else Return y
 .
 
-(** [no_nested_borrows::test3] *)
+(** [no_nested_borrows::test3]: forward function *)
 Definition test3_fwd : result unit :=
   x <- get_max_fwd 4%u32 3%u32;
   y <- get_max_fwd 10%u32 11%u32;
@@ -96,7 +96,7 @@ Definition test3_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test3] *)
 Check (test3_fwd )%return.
 
-(** [no_nested_borrows::test_neg1] *)
+(** [no_nested_borrows::test_neg1]: forward function *)
 Definition test_neg1_fwd : result unit :=
   y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt
 .
@@ -104,7 +104,7 @@ Definition test_neg1_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_neg1] *)
 Check (test_neg1_fwd )%return.
 
-(** [no_nested_borrows::refs_test1] *)
+(** [no_nested_borrows::refs_test1]: forward function *)
 Definition refs_test1_fwd : result unit :=
   if negb (1%i32 s= 1%i32) then Fail_ Failure else Return tt
 .
@@ -112,7 +112,7 @@ Definition refs_test1_fwd : result unit :=
 (** Unit test for [no_nested_borrows::refs_test1] *)
 Check (refs_test1_fwd )%return.
 
-(** [no_nested_borrows::refs_test2] *)
+(** [no_nested_borrows::refs_test2]: forward function *)
 Definition refs_test2_fwd : result unit :=
   if negb (2%i32 s= 2%i32)
   then Fail_ Failure
@@ -128,14 +128,14 @@ Definition refs_test2_fwd : result unit :=
 (** Unit test for [no_nested_borrows::refs_test2] *)
 Check (refs_test2_fwd )%return.
 
-(** [no_nested_borrows::test_list1] *)
+(** [no_nested_borrows::test_list1]: forward function *)
 Definition test_list1_fwd : result unit :=
   Return tt.
 
 (** Unit test for [no_nested_borrows::test_list1] *)
 Check (test_list1_fwd )%return.
 
-(** [no_nested_borrows::test_box1] *)
+(** [no_nested_borrows::test_box1]: forward function *)
 Definition test_box1_fwd : result unit :=
   let b := 1%i32 in
   let x := b in
@@ -145,21 +145,21 @@ Definition test_box1_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_box1] *)
 Check (test_box1_fwd )%return.
 
-(** [no_nested_borrows::copy_int] *)
+(** [no_nested_borrows::copy_int]: forward function *)
 Definition copy_int_fwd (x : i32) : result i32 :=
   Return x.
 
-(** [no_nested_borrows::test_unreachable] *)
+(** [no_nested_borrows::test_unreachable]: forward function *)
 Definition test_unreachable_fwd (b : bool) : result unit :=
   if b then Fail_ Failure else Return tt
 .
 
-(** [no_nested_borrows::test_panic] *)
+(** [no_nested_borrows::test_panic]: forward function *)
 Definition test_panic_fwd (b : bool) : result unit :=
   if b then Fail_ Failure else Return tt
 .
 
-(** [no_nested_borrows::test_copy_int] *)
+(** [no_nested_borrows::test_copy_int]: forward function *)
 Definition test_copy_int_fwd : result unit :=
   y <- copy_int_fwd 0%i32;
   if negb (0%i32 s= y) then Fail_ Failure else Return tt
@@ -168,12 +168,12 @@ Definition test_copy_int_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_copy_int] *)
 Check (test_copy_int_fwd )%return.
 
-(** [no_nested_borrows::is_cons] *)
+(** [no_nested_borrows::is_cons]: forward function *)
 Definition is_cons_fwd (T : Type) (l : List_t T) : result bool :=
   match l with | ListCons t l0 => Return true | ListNil => Return false end
 .
 
-(** [no_nested_borrows::test_is_cons] *)
+(** [no_nested_borrows::test_is_cons]: forward function *)
 Definition test_is_cons_fwd : result unit :=
   let l := ListNil in
   b <- is_cons_fwd i32 (ListCons 0%i32 l);
@@ -183,7 +183,7 @@ Definition test_is_cons_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_is_cons] *)
 Check (test_is_cons_fwd )%return.
 
-(** [no_nested_borrows::split_list] *)
+(** [no_nested_borrows::split_list]: forward function *)
 Definition split_list_fwd
   (T : Type) (l : List_t T) : result (T * (List_t T)) :=
   match l with
@@ -192,7 +192,7 @@ Definition split_list_fwd
   end
 .
 
-(** [no_nested_borrows::test_split_list] *)
+(** [no_nested_borrows::test_split_list]: forward function *)
 Definition test_split_list_fwd : result unit :=
   let l := ListNil in
   p <- split_list_fwd i32 (ListCons 0%i32 l);
@@ -203,18 +203,18 @@ Definition test_split_list_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_split_list] *)
 Check (test_split_list_fwd )%return.
 
-(** [no_nested_borrows::choose] *)
+(** [no_nested_borrows::choose]: forward function *)
 Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
   if b then Return x else Return y
 .
 
-(** [no_nested_borrows::choose] *)
+(** [no_nested_borrows::choose]: backward function 0 *)
 Definition choose_back
   (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
   if b then Return (ret, y) else Return (x, ret)
 .
 
-(** [no_nested_borrows::choose_test] *)
+(** [no_nested_borrows::choose_test]: forward function *)
 Definition choose_test_fwd : result unit :=
   z <- choose_fwd i32 true 0%i32 0%i32;
   z0 <- i32_add z 1%i32;
@@ -231,7 +231,7 @@ Definition choose_test_fwd : result unit :=
 (** Unit test for [no_nested_borrows::choose_test] *)
 Check (choose_test_fwd )%return.
 
-(** [no_nested_borrows::test_char] *)
+(** [no_nested_borrows::test_char]: forward function *)
 Definition test_char_fwd : result char :=
   Return (char_of_byte Coq.Init.Byte.x61)
 .
@@ -253,7 +253,7 @@ Arguments NodeElemNil {T}.
 Arguments TreeLeaf {T} _.
 Arguments TreeNode {T} _ _ _.
 
-(** [no_nested_borrows::list_length] *)
+(** [no_nested_borrows::list_length]: forward function *)
 Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   match l with
   | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i
@@ -261,7 +261,7 @@ Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   end
 .
 
-(** [no_nested_borrows::list_nth_shared] *)
+(** [no_nested_borrows::list_nth_shared]: forward function *)
 Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   match l with
   | ListCons x tl =>
@@ -272,7 +272,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   end
 .
 
-(** [no_nested_borrows::list_nth_mut] *)
+(** [no_nested_borrows::list_nth_mut]: forward function *)
 Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   match l with
   | ListCons x tl =>
@@ -283,7 +283,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   end
 .
 
-(** [no_nested_borrows::list_nth_mut] *)
+(** [no_nested_borrows::list_nth_mut]: backward function 0 *)
 Fixpoint list_nth_mut_back
   (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
   match l with
@@ -298,7 +298,7 @@ Fixpoint list_nth_mut_back
   end
 .
 
-(** [no_nested_borrows::list_rev_aux] *)
+(** [no_nested_borrows::list_rev_aux]: forward function *)
 Fixpoint list_rev_aux_fwd
   (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
   match li with
@@ -307,13 +307,14 @@ Fixpoint list_rev_aux_fwd
   end
 .
 
-(** [no_nested_borrows::list_rev] *)
+(** [no_nested_borrows::list_rev]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) :=
   let li := mem_replace_fwd (List_t T) l ListNil in
   list_rev_aux_fwd T li ListNil
 .
 
-(** [no_nested_borrows::test_list_functions] *)
+(** [no_nested_borrows::test_list_functions]: forward function *)
 Definition test_list_functions_fwd : result unit :=
   let l := ListNil in
   let l0 := ListCons 2%i32 l in
@@ -350,61 +351,61 @@ Definition test_list_functions_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_list_functions] *)
 Check (test_list_functions_fwd )%return.
 
-(** [no_nested_borrows::id_mut_pair1] *)
+(** [no_nested_borrows::id_mut_pair1]: forward function *)
 Definition id_mut_pair1_fwd
   (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
   Return (x, y)
 .
 
-(** [no_nested_borrows::id_mut_pair1] *)
+(** [no_nested_borrows::id_mut_pair1]: backward function 0 *)
 Definition id_mut_pair1_back
   (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 * T2)) : result (T1 * T2) :=
   let (t, t0) := ret in Return (t, t0)
 .
 
-(** [no_nested_borrows::id_mut_pair2] *)
+(** [no_nested_borrows::id_mut_pair2]: forward function *)
 Definition id_mut_pair2_fwd
   (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
   let (t, t0) := p in Return (t, t0)
 .
 
-(** [no_nested_borrows::id_mut_pair2] *)
+(** [no_nested_borrows::id_mut_pair2]: backward function 0 *)
 Definition id_mut_pair2_back
   (T1 T2 : Type) (p : (T1 * T2)) (ret : (T1 * T2)) : result (T1 * T2) :=
   let (t, t0) := ret in Return (t, t0)
 .
 
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: forward function *)
 Definition id_mut_pair3_fwd
   (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
   Return (x, y)
 .
 
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: backward function 0 *)
 Definition id_mut_pair3_back'a
   (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : result T1 :=
   Return ret
 .
 
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: backward function 1 *)
 Definition id_mut_pair3_back'b
   (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : result T2 :=
   Return ret
 .
 
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: forward function *)
 Definition id_mut_pair4_fwd
   (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
   let (t, t0) := p in Return (t, t0)
 .
 
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: backward function 0 *)
 Definition id_mut_pair4_back'a
   (T1 T2 : Type) (p : (T1 * T2)) (ret : T1) : result T1 :=
   Return ret
 .
 
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: backward function 1 *)
 Definition id_mut_pair4_back'b
   (T1 T2 : Type) (p : (T1 * T2)) (ret : T2) : result T2 :=
   Return ret
@@ -420,17 +421,17 @@ mkStruct_with_tuple_t {
 Arguments mkStruct_with_tuple_t {T1} {T2} _.
 Arguments Struct_with_tuple_p {T1} {T2}.
 
-(** [no_nested_borrows::new_tuple1] *)
+(** [no_nested_borrows::new_tuple1]: forward function *)
 Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
   Return {| Struct_with_tuple_p := (1%u32, 2%u32) |}
 .
 
-(** [no_nested_borrows::new_tuple2] *)
+(** [no_nested_borrows::new_tuple2]: forward function *)
 Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
   Return {| Struct_with_tuple_p := (1%i16, 2%i16) |}
 .
 
-(** [no_nested_borrows::new_tuple3] *)
+(** [no_nested_borrows::new_tuple3]: forward function *)
 Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
   Return {| Struct_with_tuple_p := (1%u64, 2%i64) |}
 .
@@ -445,12 +446,12 @@ mkStruct_with_pair_t {
 Arguments mkStruct_with_pair_t {T1} {T2} _.
 Arguments Struct_with_pair_p {T1} {T2}.
 
-(** [no_nested_borrows::new_pair1] *)
+(** [no_nested_borrows::new_pair1]: forward function *)
 Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
   Return {| Struct_with_pair_p := {| Pair_x := 1%u32; Pair_y := 2%u32 |} |}
 .
 
-(** [no_nested_borrows::test_constants] *)
+(** [no_nested_borrows::test_constants]: forward function *)
 Definition test_constants_fwd : result unit :=
   swt <- new_tuple1_fwd;
   let (i, _) := swt.(Struct_with_tuple_p) in
@@ -476,34 +477,35 @@ Definition test_constants_fwd : result unit :=
 (** Unit test for [no_nested_borrows::test_constants] *)
 Check (test_constants_fwd )%return.
 
-(** [no_nested_borrows::test_weird_borrows1] *)
+(** [no_nested_borrows::test_weird_borrows1]: forward function *)
 Definition test_weird_borrows1_fwd : result unit :=
   Return tt.
 
 (** Unit test for [no_nested_borrows::test_weird_borrows1] *)
 Check (test_weird_borrows1_fwd )%return.
 
-(** [no_nested_borrows::test_mem_replace] *)
+(** [no_nested_borrows::test_mem_replace]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition test_mem_replace_fwd_back (px : u32) : result u32 :=
   let y := mem_replace_fwd u32 px 1%u32 in
   if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32
 .
 
-(** [no_nested_borrows::test_shared_borrow_bool1] *)
+(** [no_nested_borrows::test_shared_borrow_bool1]: forward function *)
 Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 :=
   if b then Return 0%u32 else Return 1%u32
 .
 
-(** [no_nested_borrows::test_shared_borrow_bool2] *)
+(** [no_nested_borrows::test_shared_borrow_bool2]: forward function *)
 Definition test_shared_borrow_bool2_fwd : result u32 :=
   Return 0%u32.
 
-(** [no_nested_borrows::test_shared_borrow_enum1] *)
+(** [no_nested_borrows::test_shared_borrow_enum1]: forward function *)
 Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
   match l with | ListCons i l0 => Return 1%u32 | ListNil => Return 0%u32 end
 .
 
-(** [no_nested_borrows::test_shared_borrow_enum2] *)
+(** [no_nested_borrows::test_shared_borrow_enum2]: forward function *)
 Definition test_shared_borrow_enum2_fwd : result u32 :=
   Return 0%u32.
 
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 513bc749..0f854f31 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -6,11 +6,12 @@ Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
 Module Paper.
 
-(** [paper::ref_incr] *)
+(** [paper::ref_incr]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition ref_incr_fwd_back (x : i32) : result i32 :=
   i32_add x 1%i32.
 
-(** [paper::test_incr] *)
+(** [paper::test_incr]: forward function *)
 Definition test_incr_fwd : result unit :=
   x <- ref_incr_fwd_back 0%i32;
   if negb (x s= 1%i32) then Fail_ Failure else Return tt
@@ -19,18 +20,18 @@ Definition test_incr_fwd : result unit :=
 (** Unit test for [paper::test_incr] *)
 Check (test_incr_fwd )%return.
 
-(** [paper::choose] *)
+(** [paper::choose]: forward function *)
 Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
   if b then Return x else Return y
 .
 
-(** [paper::choose] *)
+(** [paper::choose]: backward function 0 *)
 Definition choose_back
   (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
   if b then Return (ret, y) else Return (x, ret)
 .
 
-(** [paper::test_choose] *)
+(** [paper::test_choose]: forward function *)
 Definition test_choose_fwd : result unit :=
   z <- choose_fwd i32 true 0%i32 0%i32;
   z0 <- i32_add z 1%i32;
@@ -56,7 +57,7 @@ Inductive List_t (T : Type) :=
 Arguments ListCons {T} _ _.
 Arguments ListNil {T}.
 
-(** [paper::list_nth_mut] *)
+(** [paper::list_nth_mut]: forward function *)
 Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   match l with
   | ListCons x tl =>
@@ -67,7 +68,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   end
 .
 
-(** [paper::list_nth_mut] *)
+(** [paper::list_nth_mut]: backward function 0 *)
 Fixpoint list_nth_mut_back
   (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
   match l with
@@ -82,7 +83,7 @@ Fixpoint list_nth_mut_back
   end
 .
 
-(** [paper::sum] *)
+(** [paper::sum]: forward function *)
 Fixpoint sum_fwd (l : List_t i32) : result i32 :=
   match l with
   | ListCons x tl => i <- sum_fwd tl; i32_add x i
@@ -90,7 +91,7 @@ Fixpoint sum_fwd (l : List_t i32) : result i32 :=
   end
 .
 
-(** [paper::test_nth] *)
+(** [paper::test_nth]: forward function *)
 Definition test_nth_fwd : result unit :=
   let l := ListNil in
   let l0 := ListCons 3%i32 l in
@@ -105,7 +106,7 @@ Definition test_nth_fwd : result unit :=
 (** Unit test for [paper::test_nth] *)
 Check (test_nth_fwd )%return.
 
-(** [paper::call_choose] *)
+(** [paper::call_choose]: forward function *)
 Definition call_choose_fwd (p : (u32 * u32)) : result u32 :=
   let (px, py) := p in
   pz <- choose_fwd u32 true px py;
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index bd6df02e..e94b6dcb 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -15,7 +15,7 @@ Inductive List_t (T : Type) :=
 Arguments ListCons {T} _ _.
 Arguments ListNil {T}.
 
-(** [polonius_list::get_list_at_x] *)
+(** [polonius_list::get_list_at_x]: forward function *)
 Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) :=
   match ls with
   | ListCons hd tl =>
@@ -24,7 +24,7 @@ Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) :=
   end
 .
 
-(** [polonius_list::get_list_at_x] *)
+(** [polonius_list::get_list_at_x]: backward function 0 *)
 Fixpoint get_list_at_x_back
   (ls : List_t u32) (x : u32) (ret : List_t u32) : result (List_t u32) :=
   match ls with
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 87dea3e6..db6c2742 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,12 +3,12 @@
 -arg -w
 -arg all
 
-Constants.v
-External_Types.v
-Primitives.v
 Loops.v
+Primitives.v
 External_Funs.v
+Constants.v
 PoloniusList.v
+External_Types.v
 NoNestedBorrows.v
 External_Opaque.v
 Paper.v
-- 
cgit v1.2.3