Merge pull request #31 from AeneasVerif/son_lean_backend

Improve the Lean backend

15 files changed, 328 insertions, 299 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 940b8650..86a9d5f2 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -10,7 +10,7 @@ Require Export BetreeMain_Opaque.
 Import BetreeMain_Opaque.
 Module BetreeMain_Funs.
 
-(** [betree_main::betree::load_internal_node] *)
+(** [betree_main::betree::load_internal_node]: forward function *)
 Definition betree_load_internal_node_fwd
   (id : u64) (st : state) :
   result (state * (Betree_list_t (u64 * Betree_message_t)))
@@ -18,7 +18,7 @@ Definition betree_load_internal_node_fwd
   betree_utils_load_internal_node_fwd id st
 .
 
-(** [betree_main::betree::store_internal_node] *)
+(** [betree_main::betree::store_internal_node]: forward function *)
 Definition betree_store_internal_node_fwd
   (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
   result (state * unit)
@@ -28,13 +28,13 @@ Definition betree_store_internal_node_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::load_leaf_node] *)
+(** [betree_main::betree::load_leaf_node]: forward function *)
 Definition betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) :=
   betree_utils_load_leaf_node_fwd id st
 .
 
-(** [betree_main::betree::store_leaf_node] *)
+(** [betree_main::betree::store_leaf_node]: forward function *)
 Definition betree_store_leaf_node_fwd
   (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) :
   result (state * unit)
@@ -44,29 +44,29 @@ Definition betree_store_leaf_node_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::fresh_node_id] *)
+(** [betree_main::betree::fresh_node_id]: forward function *)
 Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
   _ <- u64_add counter 1%u64; Return counter
 .
 
-(** [betree_main::betree::fresh_node_id] *)
+(** [betree_main::betree::fresh_node_id]: backward function 0 *)
 Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
   u64_add counter 1%u64
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::new] *)
+(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
 Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
   Return {| Betree_node_id_counter_next_node_id := 0%u64 |}
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
+(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
 Definition betree_node_id_counter_fresh_id_fwd
   (self : Betree_node_id_counter_t) : result u64 :=
   _ <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
   Return self.(Betree_node_id_counter_next_node_id)
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
+(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
 Definition betree_node_id_counter_fresh_id_back
   (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
   i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
@@ -79,7 +79,7 @@ Definition core_num_u64_max_body : result u64 :=
 .
 Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
 
-(** [betree_main::betree::upsert_update] *)
+(** [betree_main::betree::upsert_update]: forward function *)
 Definition betree_upsert_update_fwd
   (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 :=
   match prev with
@@ -99,7 +99,7 @@ Definition betree_upsert_update_fwd
   end
 .
 
-(** [betree_main::betree::List::{1}::len] *)
+(** [betree_main::betree::List::{1}::len]: forward function *)
 Fixpoint betree_list_len_fwd
   (T : Type) (n : nat) (self : Betree_list_t T) : result u64 :=
   match n with
@@ -112,7 +112,7 @@ Fixpoint betree_list_len_fwd
   end
 .
 
-(** [betree_main::betree::List::{1}::split_at] *)
+(** [betree_main::betree::List::{1}::split_at]: forward function *)
 Fixpoint betree_list_split_at_fwd
   (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) :
   result ((Betree_list_t T) * (Betree_list_t T))
@@ -135,7 +135,8 @@ Fixpoint betree_list_split_at_fwd
   end
 .
 
-(** [betree_main::betree::List::{1}::push_front] *)
+(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition betree_list_push_front_fwd_back
   (T : Type) (self : Betree_list_t T) (x : T) : result (Betree_list_t T) :=
   let tl := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
@@ -143,7 +144,7 @@ Definition betree_list_push_front_fwd_back
   Return (BetreeListCons x l)
 .
 
-(** [betree_main::betree::List::{1}::pop_front] *)
+(** [betree_main::betree::List::{1}::pop_front]: forward function *)
 Definition betree_list_pop_front_fwd
   (T : Type) (self : Betree_list_t T) : result T :=
   let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
@@ -153,7 +154,7 @@ Definition betree_list_pop_front_fwd
   end
 .
 
-(** [betree_main::betree::List::{1}::pop_front] *)
+(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *)
 Definition betree_list_pop_front_back
   (T : Type) (self : Betree_list_t T) : result (Betree_list_t T) :=
   let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
@@ -163,7 +164,7 @@ Definition betree_list_pop_front_back
   end
 .
 
-(** [betree_main::betree::List::{1}::hd] *)
+(** [betree_main::betree::List::{1}::hd]: forward function *)
 Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T :=
   match self with
   | BetreeListCons hd l => Return hd
@@ -171,7 +172,7 @@ Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T :=
   end
 .
 
-(** [betree_main::betree::List::{2}::head_has_key] *)
+(** [betree_main::betree::List::{2}::head_has_key]: forward function *)
 Definition betree_list_head_has_key_fwd
   (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool :=
   match self with
@@ -180,7 +181,7 @@ Definition betree_list_head_has_key_fwd
   end
 .
 
-(** [betree_main::betree::List::{2}::partition_at_pivot] *)
+(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
 Fixpoint betree_list_partition_at_pivot_fwd
   (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) :
   result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T)))
@@ -203,7 +204,7 @@ Fixpoint betree_list_partition_at_pivot_fwd
   end
 .
 
-(** [betree_main::betree::Leaf::{3}::split] *)
+(** [betree_main::betree::Leaf::{3}::split]: forward function *)
 Definition betree_leaf_split_fwd
   (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64))
   (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t)
@@ -236,7 +237,7 @@ Definition betree_leaf_split_fwd
   Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
 .
 
-(** [betree_main::betree::Leaf::{3}::split] *)
+(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
 Definition betree_leaf_split_back
   (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64))
   (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t)
@@ -257,7 +258,7 @@ Definition betree_leaf_split_back
   betree_node_id_counter_fresh_id_back node_id_cnt0
 .
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
 Fixpoint betree_node_lookup_in_bindings_fwd
   (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
   result (option u64)
@@ -279,7 +280,7 @@ Fixpoint betree_node_lookup_in_bindings_fwd
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
+(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 Fixpoint betree_node_lookup_first_message_for_key_fwd
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
   result (Betree_list_t (u64 * Betree_message_t))
@@ -298,7 +299,7 @@ Fixpoint betree_node_lookup_first_message_for_key_fwd
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
+(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
 Fixpoint betree_node_lookup_first_message_for_key_back
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t))
   (ret : Betree_list_t (u64 * Betree_message_t)) :
@@ -321,7 +322,7 @@ Fixpoint betree_node_lookup_first_message_for_key_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_upserts] *)
+(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
 Fixpoint betree_node_apply_upserts_fwd
   (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -353,7 +354,7 @@ Fixpoint betree_node_apply_upserts_fwd
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_upserts] *)
+(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
 Fixpoint betree_node_apply_upserts_back
   (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -383,7 +384,7 @@ Fixpoint betree_node_apply_upserts_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup] *)
+(** [betree_main::betree::Node::{5}::lookup]: forward function *)
 Fixpoint betree_node_lookup_fwd
   (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -455,7 +456,7 @@ Fixpoint betree_node_lookup_fwd
     end
   end
 
-(** [betree_main::betree::Node::{5}::lookup] *)
+(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
 with betree_node_lookup_back
   (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
   result Betree_node_t
@@ -524,7 +525,7 @@ with betree_node_lookup_back
     end
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
 with betree_internal_lookup_in_children_fwd
   (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -537,7 +538,7 @@ with betree_internal_lookup_in_children_fwd
     else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
 with betree_internal_lookup_in_children_back
   (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
   result Betree_internal_t
@@ -557,7 +558,7 @@ with betree_internal_lookup_in_children_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
 Fixpoint betree_node_lookup_mut_in_bindings_fwd
   (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
   result (Betree_list_t (u64 * u64))
@@ -576,7 +577,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_fwd
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
 Fixpoint betree_node_lookup_mut_in_bindings_back
   (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64))
   (ret : Betree_list_t (u64 * u64)) :
@@ -598,7 +599,8 @@ Fixpoint betree_node_lookup_mut_in_bindings_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_to_leaf] *)
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition betree_node_apply_to_leaf_fwd_back
   (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
   (new_msg : Betree_message_t) :
@@ -642,7 +644,8 @@ Definition betree_node_apply_to_leaf_fwd_back
     end
 .
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint betree_node_apply_messages_to_leaf_fwd_back
   (n : nat) (bindings : Betree_list_t (u64 * u64))
   (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
@@ -661,7 +664,8 @@ Fixpoint betree_node_apply_messages_to_leaf_fwd_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
+(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint betree_node_filter_messages_for_key_fwd_back
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
   result (Betree_list_t (u64 * Betree_message_t))
@@ -684,7 +688,7 @@ Fixpoint betree_node_filter_messages_for_key_fwd_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
+(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
 Fixpoint betree_node_lookup_first_message_after_key_fwd
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
   result (Betree_list_t (u64 * Betree_message_t))
@@ -703,7 +707,7 @@ Fixpoint betree_node_lookup_first_message_after_key_fwd
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
+(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
 Fixpoint betree_node_lookup_first_message_after_key_back
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t))
   (ret : Betree_list_t (u64 * Betree_message_t)) :
@@ -726,7 +730,8 @@ Fixpoint betree_node_lookup_first_message_after_key_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_to_internal] *)
+(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition betree_node_apply_to_internal_fwd_back
   (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64)
   (new_msg : Betree_message_t) :
@@ -784,7 +789,8 @@ Definition betree_node_apply_to_internal_fwd_back
     betree_node_lookup_first_message_for_key_back n key msgs msgs1)
 .
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
+(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint betree_node_apply_messages_to_internal_fwd_back
   (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t))
   (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
@@ -803,7 +809,7 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_messages] *)
+(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
 Fixpoint betree_node_apply_messages_fwd
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
@@ -859,7 +865,7 @@ Fixpoint betree_node_apply_messages_fwd
     end
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages] *)
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
 with betree_node_apply_messages_back
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
@@ -915,7 +921,7 @@ with betree_node_apply_messages_back
     end
   end
 
-(** [betree_main::betree::Internal::{4}::flush] *)
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
 with betree_internal_flush_fwd
   (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
@@ -963,7 +969,7 @@ with betree_internal_flush_fwd
       Return (st0, msgs_left))
   end
 
-(** [betree_main::betree::Internal::{4}::flush] *)
+(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
 with betree_internal_flush_back
   (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
@@ -1012,7 +1018,7 @@ with betree_internal_flush_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply] *)
+(** [betree_main::betree::Node::{5}::apply]: forward function *)
 Definition betree_node_apply_fwd
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t) (key : u64)
@@ -1030,7 +1036,7 @@ Definition betree_node_apply_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::Node::{5}::apply] *)
+(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
 Definition betree_node_apply_back
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t) (key : u64)
@@ -1042,7 +1048,7 @@ Definition betree_node_apply_back
     (key, new_msg) l) st
 .
 
-(** [betree_main::betree::BeTree::{6}::new] *)
+(** [betree_main::betree::BeTree::{6}::new]: forward function *)
 Definition betree_be_tree_new_fwd
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * Betree_be_tree_t)
@@ -1065,7 +1071,7 @@ Definition betree_be_tree_new_fwd
     |})
 .
 
-(** [betree_main::betree::BeTree::{6}::apply] *)
+(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
 Definition betree_be_tree_apply_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t)
   (st : state) :
@@ -1081,7 +1087,7 @@ Definition betree_be_tree_apply_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::apply] *)
+(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
 Definition betree_be_tree_apply_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t)
   (st : state) :
@@ -1099,7 +1105,7 @@ Definition betree_be_tree_apply_back
     |}
 .
 
-(** [betree_main::betree::BeTree::{6}::insert] *)
+(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
 Definition betree_be_tree_insert_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result (state * unit)
@@ -1110,7 +1116,7 @@ Definition betree_be_tree_insert_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::insert] *)
+(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
 Definition betree_be_tree_insert_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result Betree_be_tree_t
@@ -1118,7 +1124,7 @@ Definition betree_be_tree_insert_back
   betree_be_tree_apply_back n self key (BetreeMessageInsert value) st
 .
 
-(** [betree_main::betree::BeTree::{6}::delete] *)
+(** [betree_main::betree::BeTree::{6}::delete]: forward function *)
 Definition betree_be_tree_delete_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result (state * unit)
@@ -1129,7 +1135,7 @@ Definition betree_be_tree_delete_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::delete] *)
+(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
 Definition betree_be_tree_delete_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result Betree_be_tree_t
@@ -1137,7 +1143,7 @@ Definition betree_be_tree_delete_back
   betree_be_tree_apply_back n self key BetreeMessageDelete st
 .
 
-(** [betree_main::betree::BeTree::{6}::upsert] *)
+(** [betree_main::betree::BeTree::{6}::upsert]: forward function *)
 Definition betree_be_tree_upsert_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64)
   (upd : Betree_upsert_fun_state_t) (st : state) :
@@ -1149,7 +1155,7 @@ Definition betree_be_tree_upsert_fwd
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::upsert] *)
+(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
 Definition betree_be_tree_upsert_back
   (n : nat) (self : Betree_be_tree_t) (key : u64)
   (upd : Betree_upsert_fun_state_t) (st : state) :
@@ -1158,7 +1164,7 @@ Definition betree_be_tree_upsert_back
   betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st
 .
 
-(** [betree_main::betree::BeTree::{6}::lookup] *)
+(** [betree_main::betree::BeTree::{6}::lookup]: forward function *)
 Definition betree_be_tree_lookup_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -1166,7 +1172,7 @@ Definition betree_be_tree_lookup_fwd
   betree_node_lookup_fwd n self.(Betree_be_tree_root) key st
 .
 
-(** [betree_main::betree::BeTree::{6}::lookup] *)
+(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
 Definition betree_be_tree_lookup_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result Betree_be_tree_t
@@ -1180,7 +1186,7 @@ Definition betree_be_tree_lookup_back
     |}
 .
 
-(** [betree_main::main] *)
+(** [betree_main::main]: forward function *)
 Definition main_fwd : result unit :=
   Return tt.
 
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index 08ab530a..bd49500b 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -1,5 +1,5 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: opaque function definitions *)
+(** [betree_main]: external function declarations *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
@@ -8,29 +8,29 @@ Require Export BetreeMain_Types.
 Import BetreeMain_Types.
 Module BetreeMain_Opaque.
 
-(** [betree_main::betree_utils::load_internal_node] *)
+(** [betree_main::betree_utils::load_internal_node]: forward function *)
 Axiom betree_utils_load_internal_node_fwd
   : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t)))
 .
 
-(** [betree_main::betree_utils::store_internal_node] *)
+(** [betree_main::betree_utils::store_internal_node]: forward function *)
 Axiom betree_utils_store_internal_node_fwd
   :
   u64 -> Betree_list_t (u64 * Betree_message_t) -> state -> result (state *
     unit)
 .
 
-(** [betree_main::betree_utils::load_leaf_node] *)
+(** [betree_main::betree_utils::load_leaf_node]: forward function *)
 Axiom betree_utils_load_leaf_node_fwd
   : u64 -> state -> result (state * (Betree_list_t (u64 * u64)))
 .
 
-(** [betree_main::betree_utils::store_leaf_node] *)
+(** [betree_main::betree_utils::store_leaf_node]: forward function *)
 Axiom betree_utils_store_leaf_node_fwd
   : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit)
 .
 
-(** [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/betree/_CoqProject b/tests/coq/betree/_CoqProject
index e5a3f799..42c62421 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,7 +3,7 @@
 -arg -w
 -arg all
 
-Primitives.v
 BetreeMain_Types.v
+Primitives.v
 BetreeMain_Funs.v
 BetreeMain_Opaque.v
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 6bc82677..c8630eb6 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -8,11 +8,11 @@ Require Export Hashmap_Types.
 Import Hashmap_Types.
 Module Hashmap_Funs.
 
-(** [hashmap::hash_key] *)
+(** [hashmap::hash_key]: forward function *)
 Definition hash_key_fwd (k : usize) : result usize :=
   Return k.
 
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
 Fixpoint hash_map_allocate_slots_loop_fwd
   (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
   result (vec (List_t T))
@@ -29,7 +29,7 @@ Fixpoint hash_map_allocate_slots_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: forward function *)
 Definition hash_map_allocate_slots_fwd
   (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
   result (vec (List_t T))
@@ -37,7 +37,7 @@ Definition hash_map_allocate_slots_fwd
   hash_map_allocate_slots_loop_fwd T n slots n0
 .
 
-(** [hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap::HashMap::{0}::new_with_capacity]: forward function *)
 Definition hash_map_new_with_capacity_fwd
   (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -56,12 +56,13 @@ Definition hash_map_new_with_capacity_fwd
     |}
 .
 
-(** [hashmap::HashMap::{0}::new] *)
+(** [hashmap::HashMap::{0}::new]: forward function *)
 Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
   hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
 .
 
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hash_map_clear_loop_fwd_back
   (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
   result (vec (List_t T))
@@ -79,7 +80,8 @@ Fixpoint hash_map_clear_loop_fwd_back
   end
 .
 
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
   v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) 0%usize;
@@ -92,12 +94,12 @@ Definition hash_map_clear_fwd_back
     |}
 .
 
-(** [hashmap::HashMap::{0}::len] *)
+(** [hashmap::HashMap::{0}::len]: forward function *)
 Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize :=
   Return self.(Hash_map_num_entries)
 .
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
 Fixpoint hash_map_insert_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result bool
@@ -115,7 +117,7 @@ Fixpoint hash_map_insert_in_list_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: forward function *)
 Definition hash_map_insert_in_list_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result bool
@@ -123,7 +125,7 @@ Definition hash_map_insert_in_list_fwd
   hash_map_insert_in_list_loop_fwd T n key value ls
 .
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
 Fixpoint hash_map_insert_in_list_loop_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result (List_t T)
@@ -143,7 +145,7 @@ Fixpoint hash_map_insert_in_list_loop_back
   end
 .
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
 Definition hash_map_insert_in_list_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result (List_t T)
@@ -151,7 +153,8 @@ Definition hash_map_insert_in_list_back
   hash_map_insert_in_list_loop_back T n key value ls
 .
 
-(** [hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_insert_no_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
   result (Hash_map_t T)
@@ -189,7 +192,8 @@ Definition hash_map_insert_no_resize_fwd_back
 Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
 Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hash_map_move_elements_from_list_loop_fwd_back
   (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
   result (Hash_map_t T)
@@ -206,7 +210,8 @@ Fixpoint hash_map_move_elements_from_list_loop_fwd_back
   end
 .
 
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_move_elements_from_list_fwd_back
   (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
   result (Hash_map_t T)
@@ -214,7 +219,8 @@ Definition hash_map_move_elements_from_list_fwd_back
   hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
 .
 
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hash_map_move_elements_loop_fwd_back
   (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
   (i : usize) :
@@ -237,7 +243,8 @@ Fixpoint hash_map_move_elements_loop_fwd_back
   end
 .
 
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_move_elements_fwd_back
   (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
   (i : usize) :
@@ -246,7 +253,8 @@ Definition hash_map_move_elements_fwd_back
   hash_map_move_elements_loop_fwd_back T n ntable slots i
 .
 
-(** [hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
   max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
@@ -278,7 +286,8 @@ Definition hash_map_try_resize_fwd_back
       |}
 .
 
-(** [hashmap::HashMap::{0}::insert] *)
+(** [hashmap::HashMap::{0}::insert]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_insert_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
   result (Hash_map_t T)
@@ -290,7 +299,7 @@ Definition hash_map_insert_fwd_back
   else Return self0
 .
 
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
 Fixpoint hash_map_contains_key_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
   match n with
@@ -306,13 +315,13 @@ Fixpoint hash_map_contains_key_in_list_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
 Definition hash_map_contains_key_in_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
   hash_map_contains_key_in_list_loop_fwd T n key ls
 .
 
-(** [hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap::HashMap::{0}::contains_key]: forward function *)
 Definition hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
   hash <- hash_key_fwd key;
@@ -322,7 +331,7 @@ Definition hash_map_contains_key_fwd
   hash_map_contains_key_in_list_fwd T n key l
 .
 
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
 Fixpoint hash_map_get_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   match n with
@@ -338,13 +347,13 @@ Fixpoint hash_map_get_in_list_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: forward function *)
 Definition hash_map_get_in_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   hash_map_get_in_list_loop_fwd T n key ls
 .
 
-(** [hashmap::HashMap::{0}::get] *)
+(** [hashmap::HashMap::{0}::get]: forward function *)
 Definition hash_map_get_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
   hash <- hash_key_fwd key;
@@ -354,7 +363,7 @@ Definition hash_map_get_fwd
   hash_map_get_in_list_fwd T n key l
 .
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
 Fixpoint hash_map_get_mut_in_list_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
   match n with
@@ -370,13 +379,13 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
 Definition hash_map_get_mut_in_list_fwd
   (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
   hash_map_get_mut_in_list_loop_fwd T n ls key
 .
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
 Fixpoint hash_map_get_mut_in_list_loop_back
   (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
   result (List_t T)
@@ -396,7 +405,7 @@ Fixpoint hash_map_get_mut_in_list_loop_back
   end
 .
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
 Definition hash_map_get_mut_in_list_back
   (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
   result (List_t T)
@@ -404,7 +413,7 @@ Definition hash_map_get_mut_in_list_back
   hash_map_get_mut_in_list_loop_back T n ls key ret
 .
 
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: forward function *)
 Definition hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
   hash <- hash_key_fwd key;
@@ -414,7 +423,7 @@ Definition hash_map_get_mut_fwd
   hash_map_get_mut_in_list_fwd T n l key
 .
 
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: backward function 0 *)
 Definition hash_map_get_mut_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) :
   result (Hash_map_t T)
@@ -434,7 +443,7 @@ Definition hash_map_get_mut_back
     |}
 .
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
 Fixpoint hash_map_remove_from_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
   match n with
@@ -455,13 +464,13 @@ Fixpoint hash_map_remove_from_list_loop_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: forward function *)
 Definition hash_map_remove_from_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
   hash_map_remove_from_list_loop_fwd T n key ls
 .
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
 Fixpoint hash_map_remove_from_list_loop_back
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
   match n with
@@ -484,13 +493,13 @@ Fixpoint hash_map_remove_from_list_loop_back
   end
 .
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
 Definition hash_map_remove_from_list_back
   (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
   hash_map_remove_from_list_loop_back T n key ls
 .
 
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: forward function *)
 Definition hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
   result (option T)
@@ -507,7 +516,7 @@ Definition hash_map_remove_fwd
   end
 .
 
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: backward function 0 *)
 Definition hash_map_remove_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
   result (Hash_map_t T)
@@ -542,7 +551,7 @@ Definition hash_map_remove_back
   end
 .
 
-(** [hashmap::test1] *)
+(** [hashmap::test1]: forward function *)
 Definition test1_fwd (n : nat) : result unit :=
   hm <- hash_map_new_fwd u64 n;
   hm0 <- hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index daa9b2ba..7f80afbf 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -3,6 +3,6 @@
 -arg -w
 -arg all
 
-Primitives.v
 Hashmap_Types.v
+Primitives.v
 Hashmap_Funs.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2d1bcda6..1b7304cc 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -10,11 +10,11 @@ Require Export HashmapMain_Opaque.
 Import HashmapMain_Opaque.
 Module HashmapMain_Funs.
 
-(** [hashmap_main::hashmap::hash_key] *)
+(** [hashmap_main::hashmap::hash_key]: forward function *)
 Definition hashmap_hash_key_fwd (k : usize) : result usize :=
   Return k.
 
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
   (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
   result (vec (Hashmap_list_t T))
@@ -31,7 +31,7 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
 Definition hashmap_hash_map_allocate_slots_fwd
   (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
   result (vec (Hashmap_list_t T))
@@ -39,7 +39,7 @@ Definition hashmap_hash_map_allocate_slots_fwd
   hashmap_hash_map_allocate_slots_loop_fwd T n slots n0
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
 Definition hashmap_hash_map_new_with_capacity_fwd
   (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -58,13 +58,14 @@ Definition hashmap_hash_map_new_with_capacity_fwd
     |}
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
 Definition hashmap_hash_map_new_fwd
   (T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
   hashmap_hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hashmap_hash_map_clear_loop_fwd_back
   (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
   result (vec (Hashmap_list_t T))
@@ -82,7 +83,8 @@ Fixpoint hashmap_hash_map_clear_loop_fwd_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
@@ -100,13 +102,13 @@ Definition hashmap_hash_map_clear_fwd_back
     |}
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
 Definition hashmap_hash_map_len_fwd
   (T : Type) (self : Hashmap_hash_map_t T) : result usize :=
   Return self.(Hashmap_hash_map_num_entries)
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result bool
@@ -124,7 +126,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
 Definition hashmap_hash_map_insert_in_list_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result bool
@@ -132,7 +134,7 @@ Definition hashmap_hash_map_insert_in_list_fwd
   hashmap_hash_map_insert_in_list_loop_fwd T n key value ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
 Fixpoint hashmap_hash_map_insert_in_list_loop_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
@@ -153,7 +155,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
 Definition hashmap_hash_map_insert_in_list_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
@@ -161,7 +163,8 @@ Definition hashmap_hash_map_insert_in_list_back
   hashmap_hash_map_insert_in_list_loop_back T n key value ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_insert_no_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
   :
@@ -207,7 +210,8 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
 Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
 Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
   (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
   :
@@ -225,7 +229,8 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_move_elements_from_list_fwd_back
   (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
   :
@@ -234,7 +239,8 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back
   hashmap_hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
   (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
   (slots : vec (Hashmap_list_t T)) (i : usize) :
@@ -258,7 +264,8 @@ Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_move_elements_fwd_back
   (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
   (slots : vec (Hashmap_list_t T)) (i : usize) :
@@ -267,7 +274,8 @@ Definition hashmap_hash_map_move_elements_fwd_back
   hashmap_hash_map_move_elements_loop_fwd_back T n ntable slots i
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
@@ -302,7 +310,8 @@ Definition hashmap_hash_map_try_resize_fwd_back
       |}
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 Definition hashmap_hash_map_insert_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
   :
@@ -315,7 +324,7 @@ Definition hashmap_hash_map_insert_fwd_back
   else Return self0
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
   match n with
@@ -331,13 +340,13 @@ Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
 Definition hashmap_hash_map_contains_key_in_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
   hashmap_hash_map_contains_key_in_list_loop_fwd T n key ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
 Definition hashmap_hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result bool
@@ -349,7 +358,7 @@ Definition hashmap_hash_map_contains_key_fwd
   hashmap_hash_map_contains_key_in_list_fwd T n key l
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_get_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
@@ -365,13 +374,13 @@ Fixpoint hashmap_hash_map_get_in_list_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
 Definition hashmap_hash_map_get_in_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   hashmap_hash_map_get_in_list_loop_fwd T n key ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
 Definition hashmap_hash_map_get_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result T
@@ -383,7 +392,7 @@ Definition hashmap_hash_map_get_fwd
   hashmap_hash_map_get_in_list_fwd T n key l
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
   match n with
@@ -399,13 +408,13 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
 Definition hashmap_hash_map_get_mut_in_list_fwd
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
   hashmap_hash_map_get_mut_in_list_loop_fwd T n ls key
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
   result (Hashmap_list_t T)
@@ -425,7 +434,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
 Definition hashmap_hash_map_get_mut_in_list_back
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
   result (Hashmap_list_t T)
@@ -433,7 +442,7 @@ Definition hashmap_hash_map_get_mut_in_list_back
   hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
 Definition hashmap_hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result T
@@ -446,7 +455,7 @@ Definition hashmap_hash_map_get_mut_fwd
   hashmap_hash_map_get_mut_in_list_fwd T n l key
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
 Definition hashmap_hash_map_get_mut_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) :
   result (Hashmap_hash_map_t T)
@@ -470,7 +479,7 @@ Definition hashmap_hash_map_get_mut_back
     |}
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
 Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (option T)
@@ -495,7 +504,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
 Definition hashmap_hash_map_remove_from_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (option T)
@@ -503,7 +512,7 @@ Definition hashmap_hash_map_remove_from_list_fwd
   hashmap_hash_map_remove_from_list_loop_fwd T n key ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
 Fixpoint hashmap_hash_map_remove_from_list_loop_back
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
@@ -530,7 +539,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
 Definition hashmap_hash_map_remove_from_list_back
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
@@ -538,7 +547,7 @@ Definition hashmap_hash_map_remove_from_list_back
   hashmap_hash_map_remove_from_list_loop_back T n key ls
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
 Definition hashmap_hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result (option T)
@@ -557,7 +566,7 @@ Definition hashmap_hash_map_remove_fwd
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
 Definition hashmap_hash_map_remove_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result (Hashmap_hash_map_t T)
@@ -599,7 +608,7 @@ Definition hashmap_hash_map_remove_back
   end
 .
 
-(** [hashmap_main::hashmap::test1] *)
+(** [hashmap_main::hashmap::test1]: forward function *)
 Definition hashmap_test1_fwd (n : nat) : result unit :=
   hm <- hashmap_hash_map_new_fwd u64 n;
   hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
@@ -636,7 +645,7 @@ Definition hashmap_test1_fwd (n : nat) : result unit :=
       end))
 .
 
-(** [hashmap_main::insert_on_disk] *)
+(** [hashmap_main::insert_on_disk]: forward function *)
 Definition insert_on_disk_fwd
   (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
   p <- hashmap_utils_deserialize_fwd st;
@@ -647,7 +656,7 @@ Definition insert_on_disk_fwd
   Return (st1, tt)
 .
 
-(** [hashmap_main::main] *)
+(** [hashmap_main::main]: forward function *)
 Definition main_fwd : result unit :=
   Return tt.
 
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
index 6152b94b..1ad9c697 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -1,5 +1,5 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
+(** [hashmap_main]: external function declarations *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
@@ -8,12 +8,12 @@ Require Export HashmapMain_Types.
 Import HashmapMain_Types.
 Module HashmapMain_Opaque.
 
-(** [hashmap_main::hashmap_utils::deserialize] *)
+(** [hashmap_main::hashmap_utils::deserialize]: forward function *)
 Axiom hashmap_utils_deserialize_fwd
   : state -> result (state * (Hashmap_hash_map_t u64))
 .
 
-(** [hashmap_main::hashmap_utils::serialize] *)
+(** [hashmap_main::hashmap_utils::serialize]: forward function *)
 Axiom hashmap_utils_serialize_fwd
   : Hashmap_hash_map_t u64 -> state -> result (state * unit)
 .
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 d60251e0..1224f426 100644
--- a/tests/coq/misc/External_Opaque.v
+++ b/tests/coq/misc/External_Opaque.v
@@ -1,5 +1,5 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: opaque function definitions *)
+(** [external]: external function declarations *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
@@ -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