Merge pull request #213 from AeneasVerif/cleanup-tests

7 files changed, 84 insertions, 84 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/Betree_Funs.v
index e0a1d8a2..b965d423 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -1,18 +1,18 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: function definitions *)
+(** [betree]: function definitions *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Import BetreeMain_Types.
-Include BetreeMain_Types.
-Require Import BetreeMain_FunsExternal.
-Include BetreeMain_FunsExternal.
-Module BetreeMain_Funs.
+Require Import Betree_Types.
+Include Betree_Types.
+Require Import Betree_FunsExternal.
+Include Betree_FunsExternal.
+Module Betree_Funs.
 
-(** [betree_main::betree::load_internal_node]:
+(** [betree::betree::load_internal_node]:
     Source: 'src/betree.rs', lines 36:0-36:52 *)
 Definition betree_load_internal_node
   (id : u64) (st : state) :
@@ -21,7 +21,7 @@ Definition betree_load_internal_node
   betree_utils_load_internal_node id st
 .
 
-(** [betree_main::betree::store_internal_node]:
+(** [betree::betree::store_internal_node]:
     Source: 'src/betree.rs', lines 41:0-41:60 *)
 Definition betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
@@ -30,14 +30,14 @@ Definition betree_store_internal_node
   betree_utils_store_internal_node id content st
 .
 
-(** [betree_main::betree::load_leaf_node]:
+(** [betree::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
 Definition betree_load_leaf_node
   (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) :=
   betree_utils_load_leaf_node id st
 .
 
-(** [betree_main::betree::store_leaf_node]:
+(** [betree::betree::store_leaf_node]:
     Source: 'src/betree.rs', lines 51:0-51:52 *)
 Definition betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
@@ -46,19 +46,19 @@ Definition betree_store_leaf_node
   betree_utils_store_leaf_node id content st
 .
 
-(** [betree_main::betree::fresh_node_id]:
+(** [betree::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
 Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) :=
   counter1 <- u64_add counter 1%u64; Ok (counter, counter1)
 .
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
+(** [betree::betree::{betree::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
   Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
+(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]:
     Source: 'src/betree.rs', lines 210:4-210:36 *)
 Definition betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) :=
@@ -67,7 +67,7 @@ Definition betree_NodeIdCounter_fresh_id
     {| betree_NodeIdCounter_next_node_id := i |})
 .
 
-(** [betree_main::betree::upsert_update]:
+(** [betree::betree::upsert_update]:
     Source: 'src/betree.rs', lines 234:0-234:70 *)
 Definition betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 :=
@@ -88,7 +88,7 @@ Definition betree_upsert_update
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
+(** [betree::betree::{betree::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
 Fixpoint betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
@@ -102,7 +102,7 @@ Fixpoint betree_List_len
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
     Source: 'src/betree.rs', lines 284:4-284:51 *)
 Fixpoint betree_List_split_at
   (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
@@ -125,7 +125,7 @@ Fixpoint betree_List_split_at
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
+(** [betree::betree::{betree::betree::List<T>#1}::push_front]:
     Source: 'src/betree.rs', lines 299:4-299:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
@@ -133,7 +133,7 @@ Definition betree_List_push_front
   Ok (Betree_List_Cons x tl)
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
+(** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 306:4-306:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
@@ -144,7 +144,7 @@ Definition betree_List_pop_front
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
+(** [betree::betree::{betree::betree::List<T>#1}::hd]:
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
@@ -153,7 +153,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
 Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
@@ -163,7 +163,7 @@ Definition betree_ListPairU64T_head_has_key
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 Fixpoint betree_ListPairU64T_partition_at_pivot
   (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
@@ -186,7 +186,7 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
+(** [betree::betree::{betree::betree::Leaf#3}::split]:
     Source: 'src/betree.rs', lines 359:4-364:17 *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
@@ -222,7 +222,7 @@ Definition betree_Leaf_split
     node_id_cnt2))
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
     Source: 'src/betree.rs', lines 789:4-792:34 *)
 Fixpoint betree_Node_lookup_first_message_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -250,7 +250,7 @@ Fixpoint betree_Node_lookup_first_message_for_key
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
     Source: 'src/betree.rs', lines 636:4-636:80 *)
 Fixpoint betree_Node_lookup_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
@@ -271,7 +271,7 @@ Fixpoint betree_Node_lookup_in_bindings
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 Fixpoint betree_Node_apply_upserts
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
@@ -303,7 +303,7 @@ Fixpoint betree_Node_apply_upserts
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
+(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
@@ -327,7 +327,7 @@ Fixpoint betree_Internal_lookup_in_children
         self.(betree_Internal_pivot) self.(betree_Internal_left) n2)))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
+(** [betree::betree::{betree::betree::Node#5}::lookup]:
     Source: 'src/betree.rs', lines 709:4-709:58 *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
@@ -394,7 +394,7 @@ with betree_Node_lookup
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
     Source: 'src/betree.rs', lines 674:4-674:77 *)
 Fixpoint betree_Node_filter_messages_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -419,7 +419,7 @@ Fixpoint betree_Node_filter_messages_for_key
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
     Source: 'src/betree.rs', lines 689:4-692:34 *)
 Fixpoint betree_Node_lookup_first_message_after_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -447,7 +447,7 @@ Fixpoint betree_Node_lookup_first_message_after_key
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
+(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
     Source: 'src/betree.rs', lines 521:4-521:89 *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
@@ -508,7 +508,7 @@ Definition betree_Node_apply_to_internal
     lookup_first_message_for_key_back msgs2)
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
     Source: 'src/betree.rs', lines 502:4-505:5 *)
 Fixpoint betree_Node_apply_messages_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
@@ -528,7 +528,7 @@ Fixpoint betree_Node_apply_messages_to_internal
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
     Source: 'src/betree.rs', lines 653:4-656:32 *)
 Fixpoint betree_Node_lookup_mut_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
@@ -556,7 +556,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
+(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
     Source: 'src/betree.rs', lines 460:4-460:87 *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
@@ -594,7 +594,7 @@ Definition betree_Node_apply_to_leaf
     end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
     Source: 'src/betree.rs', lines 444:4-447:5 *)
 Fixpoint betree_Node_apply_messages_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64))
@@ -614,7 +614,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
+(** [betree::betree::{betree::betree::Internal#4}::flush]:
     Source: 'src/betree.rs', lines 410:4-415:26 *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
@@ -664,7 +664,7 @@ Fixpoint betree_Internal_flush
         node_id_cnt1))))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
+(** [betree::betree::{betree::betree::Node#5}::apply_messages]:
     Source: 'src/betree.rs', lines 588:4-593:5 *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
@@ -720,7 +720,7 @@ with betree_Node_apply_messages
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]:
+(** [betree::betree::{betree::betree::Node#5}::apply]:
     Source: 'src/betree.rs', lines 576:4-582:5 *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
@@ -736,7 +736,7 @@ Definition betree_Node_apply
   Ok (st1, (self1, node_id_cnt1))
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
+(** [betree::betree::{betree::betree::BeTree#6}::new]:
     Source: 'src/betree.rs', lines 849:4-849:60 *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
@@ -761,7 +761,7 @@ Definition betree_BeTree_new
     |})
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
+(** [betree::betree::{betree::betree::BeTree#6}::apply]:
     Source: 'src/betree.rs', lines 868:4-868:47 *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
@@ -781,7 +781,7 @@ Definition betree_BeTree_apply
     |})
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
+(** [betree::betree::{betree::betree::BeTree#6}::insert]:
     Source: 'src/betree.rs', lines 874:4-874:52 *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
@@ -790,7 +790,7 @@ Definition betree_BeTree_insert
   betree_BeTree_apply n self key (Betree_Message_Insert value) st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
+(** [betree::betree::{betree::betree::BeTree#6}::delete]:
     Source: 'src/betree.rs', lines 880:4-880:38 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
@@ -799,7 +799,7 @@ Definition betree_BeTree_delete
   betree_BeTree_apply n self key Betree_Message_Delete st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
+(** [betree::betree::{betree::betree::BeTree#6}::upsert]:
     Source: 'src/betree.rs', lines 886:4-886:59 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
@@ -809,7 +809,7 @@ Definition betree_BeTree_upsert
   betree_BeTree_apply n self key (Betree_Message_Upsert upd) st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
+(** [betree::betree::{betree::betree::BeTree#6}::lookup]:
     Source: 'src/betree.rs', lines 895:4-895:62 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
@@ -826,12 +826,12 @@ Definition betree_BeTree_lookup
     |}))
 .
 
-(** [betree_main::main]:
+(** [betree::main]:
     Source: 'src/main.rs', lines 4:0-4:9 *)
 Definition main : result unit :=
   Ok tt.
 
-(** Unit test for [betree_main::main] *)
+(** Unit test for [betree::main] *)
 Check (main )%return.
 
-End BetreeMain_Funs.
+End Betree_Funs.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/Betree_FunsExternal.v
index 099a2e8f..0263c272 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal.v
+++ b/tests/coq/betree/Betree_FunsExternal.v
@@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
-Module BetreeMain_FunsExternal.
+Require Export Betree_Types.
+Import Betree_Types.
+Module Betree_FunsExternal.
 
 (** [betree_main::betree_utils::load_internal_node]: forward function
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
@@ -36,4 +36,4 @@ Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-End BetreeMain_FunsExternal.
+End Betree_FunsExternal.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/Betree_FunsExternal_Template.v
index 58be2733..2a2fddfc 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/Betree_FunsExternal_Template.v
@@ -1,5 +1,5 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external functions.
+(** [betree]: external functions.
 -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
 Require Import Primitives.
 Import Primitives.
@@ -7,17 +7,17 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Import BetreeMain_Types.
-Include BetreeMain_Types.
-Module BetreeMain_FunsExternal_Template.
+Require Import Betree_Types.
+Include Betree_Types.
+Module Betree_FunsExternal_Template.
 
-(** [betree_main::betree_utils::load_internal_node]:
+(** [betree::betree_utils::load_internal_node]:
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 Axiom betree_utils_load_internal_node
   : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
 .
 
-(** [betree_main::betree_utils::store_internal_node]:
+(** [betree::betree_utils::store_internal_node]:
     Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 Axiom betree_utils_store_internal_node
   :
@@ -25,16 +25,16 @@ Axiom betree_utils_store_internal_node
     unit)
 .
 
-(** [betree_main::betree_utils::load_leaf_node]:
+(** [betree::betree_utils::load_leaf_node]:
     Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 Axiom betree_utils_load_leaf_node
   : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
 .
 
-(** [betree_main::betree_utils::store_leaf_node]:
+(** [betree::betree_utils::store_leaf_node]:
     Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-End BetreeMain_FunsExternal_Template.
+End Betree_FunsExternal_Template.
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/Betree_Types.v
index acbc2085..aa39d8e4 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/Betree_Types.v
@@ -1,16 +1,16 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
+(** [betree]: type definitions *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Import BetreeMain_TypesExternal.
-Include BetreeMain_TypesExternal.
-Module BetreeMain_Types.
+Require Import Betree_TypesExternal.
+Include Betree_TypesExternal.
+Module Betree_Types.
 
-(** [betree_main::betree::List]
+(** [betree::betree::List]
     Source: 'src/betree.rs', lines 17:0-17:23 *)
 Inductive betree_List_t (T : Type) :=
 | Betree_List_Cons : T -> betree_List_t T -> betree_List_t T
@@ -20,14 +20,14 @@ Inductive betree_List_t (T : Type) :=
 Arguments Betree_List_Cons { _ }.
 Arguments Betree_List_Nil { _ }.
 
-(** [betree_main::betree::UpsertFunState]
+(** [betree::betree::UpsertFunState]
     Source: 'src/betree.rs', lines 63:0-63:23 *)
 Inductive betree_UpsertFunState_t :=
 | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
 | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
 .
 
-(** [betree_main::betree::Message]
+(** [betree::betree::Message]
     Source: 'src/betree.rs', lines 69:0-69:23 *)
 Inductive betree_Message_t :=
 | Betree_Message_Insert : u64 -> betree_Message_t
@@ -35,7 +35,7 @@ Inductive betree_Message_t :=
 | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
 .
 
-(** [betree_main::betree::Leaf]
+(** [betree::betree::Leaf]
     Source: 'src/betree.rs', lines 167:0-167:11 *)
 Record betree_Leaf_t :=
 mkbetree_Leaf_t {
@@ -43,7 +43,7 @@ mkbetree_Leaf_t {
 }
 .
 
-(** [betree_main::betree::Internal]
+(** [betree::betree::Internal]
     Source: 'src/betree.rs', lines 156:0-156:15 *)
 Inductive betree_Internal_t :=
 | mkbetree_Internal_t :
@@ -53,7 +53,7 @@ Inductive betree_Internal_t :=
   betree_Node_t ->
   betree_Internal_t
 
-(** [betree_main::betree::Node]
+(** [betree::betree::Node]
     Source: 'src/betree.rs', lines 179:0-179:9 *)
 with betree_Node_t :=
 | Betree_Node_Internal : betree_Internal_t -> betree_Node_t
@@ -89,7 +89,7 @@ Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2)
   (at level 9)
 .
 
-(** [betree_main::betree::Params]
+(** [betree::betree::Params]
     Source: 'src/betree.rs', lines 187:0-187:13 *)
 Record betree_Params_t :=
 mkbetree_Params_t {
@@ -97,7 +97,7 @@ mkbetree_Params_t {
 }
 .
 
-(** [betree_main::betree::NodeIdCounter]
+(** [betree::betree::NodeIdCounter]
     Source: 'src/betree.rs', lines 201:0-201:20 *)
 Record betree_NodeIdCounter_t :=
 mkbetree_NodeIdCounter_t {
@@ -105,7 +105,7 @@ mkbetree_NodeIdCounter_t {
 }
 .
 
-(** [betree_main::betree::BeTree]
+(** [betree::betree::BeTree]
     Source: 'src/betree.rs', lines 218:0-218:17 *)
 Record betree_BeTree_t :=
 mkbetree_BeTree_t {
@@ -115,4 +115,4 @@ mkbetree_BeTree_t {
 }
 .
 
-End BetreeMain_Types.
+End Betree_Types.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/Betree_TypesExternal.v
index 870d2601..37487d6d 100644
--- a/tests/coq/betree/BetreeMain_TypesExternal.v
+++ b/tests/coq/betree/Betree_TypesExternal.v
@@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Module BetreeMain_TypesExternal.
+Module Betree_TypesExternal.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
 
-End BetreeMain_TypesExternal.
+End Betree_TypesExternal.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/Betree_TypesExternal_Template.v
index 651de2b7..a40811cb 100644
--- a/tests/coq/betree/BetreeMain_TypesExternal_Template.v
+++ b/tests/coq/betree/Betree_TypesExternal_Template.v
@@ -1,5 +1,5 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external types.
+(** [betree]: external types.
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
 Require Import Primitives.
 Import Primitives.
@@ -7,9 +7,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Module BetreeMain_TypesExternal_Template.
+Module Betree_TypesExternal_Template.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
 
-End BetreeMain_TypesExternal_Template.
+End Betree_TypesExternal_Template.
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index b14bed66..9fb7fe64 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,10 +3,10 @@
 -arg -w
 -arg all
 
-BetreeMain_TypesExternal_Template.v
-BetreeMain_Types.v
+Betree_TypesExternal_Template.v
+Betree_Types.v
 Primitives.v
-BetreeMain_FunsExternal_Template.v
-BetreeMain_Funs.v
-BetreeMain_TypesExternal.v
-BetreeMain_FunsExternal.v
+Betree_FunsExternal_Template.v
+Betree_Funs.v
+Betree_TypesExternal.v
+Betree_FunsExternal.v