tests: Rename betree_main -> betree

6 files changed, 85 insertions, 85 deletions

diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index b317dca4..fad8c5ba 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -1,46 +1,46 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: templates for the decreases clauses *)
-module BetreeMain.Clauses.Template
+(** [betree]: templates for the decreases clauses *)
+module Betree.Clauses.Template
 open Primitives
-open BetreeMain.Types
+open Betree.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause
+(** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause
     Source: 'src/betree.rs', lines 276:4-276:24 *)
 unfold
 let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
     Source: 'src/betree.rs', lines 284:4-284:51 *)
 unfold
 let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
   (n : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 unfold
 let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause
     Source: 'src/betree.rs', lines 789:4-792:34 *)
 unfold
 let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause
     Source: 'src/betree.rs', lines 636:4-636:80 *)
 unfold
 let betree_Node_lookup_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 unfold
 let betree_Node_apply_upserts_decreases
@@ -48,35 +48,35 @@ let betree_Node_apply_upserts_decreases
   (key : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
+(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause
     Source: 'src/betree.rs', lines 709:4-709:58 *)
 unfold
 let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause
     Source: 'src/betree.rs', lines 674:4-674:77 *)
 unfold
 let betree_Node_filter_messages_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause
     Source: 'src/betree.rs', lines 689:4-692:34 *)
 unfold
 let betree_Node_lookup_first_message_after_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause
     Source: 'src/betree.rs', lines 502:4-505:5 *)
 unfold
 let betree_Node_apply_messages_to_internal_decreases
@@ -84,14 +84,14 @@ let betree_Node_apply_messages_to_internal_decreases
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
     Source: 'src/betree.rs', lines 653:4-656:32 *)
 unfold
 let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause
     Source: 'src/betree.rs', lines 444:4-447:5 *)
 unfold
 let betree_Node_apply_messages_to_leaf_decreases
@@ -99,7 +99,7 @@ let betree_Node_apply_messages_to_leaf_decreases
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause
+(** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause
     Source: 'src/betree.rs', lines 410:4-415:26 *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
@@ -107,7 +107,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t)
   (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause
+(** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause
     Source: 'src/betree.rs', lines 588:4-593:5 *)
 unfold
 let betree_Node_apply_messages_decreases (self : betree_Node_t)
diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst
index b95d4c7e..ae201cee 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/Betree.Clauses.fst
@@ -1,7 +1,7 @@
 (** [betree_main]: templates for the decreases clauses *)
-module BetreeMain.Clauses
+module Betree.Clauses
 open Primitives
-open BetreeMain.Types
+open Betree.Types
 
 #set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
 
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index 9942ef68..07f561f5 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -1,14 +1,14 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: function definitions *)
-module BetreeMain.Funs
+(** [betree]: function definitions *)
+module Betree.Funs
 open Primitives
-include BetreeMain.Types
-include BetreeMain.FunsExternal
-include BetreeMain.Clauses
+include Betree.Types
+include Betree.FunsExternal
+include Betree.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::load_internal_node]:
+(** [betree::betree::load_internal_node]:
     Source: 'src/betree.rs', lines 36:0-36:52 *)
 let betree_load_internal_node
   (id : u64) (st : state) :
@@ -16,7 +16,7 @@ let 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 *)
 let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
@@ -24,13 +24,13 @@ let 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 *)
 let 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 *)
 let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
@@ -38,24 +38,24 @@ let 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 *)
 let betree_fresh_node_id (counter : u64) : result (u64 & u64) =
   let* counter1 = u64_add counter 1 in 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 *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Ok { next_node_id = 0 }
 
-(** [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 *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) =
   let* i = u64_add self.next_node_id 1 in
   Ok (self.next_node_id, { next_node_id = i })
 
-(** [betree_main::betree::upsert_update]:
+(** [betree::betree::upsert_update]:
     Source: 'src/betree.rs', lines 234:0-234:70 *)
 let betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 =
@@ -75,7 +75,7 @@ let betree_upsert_update
     end
   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 *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
@@ -86,7 +86,7 @@ let rec betree_List_len
   | Betree_List_Nil -> Ok 0
   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 *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
@@ -105,14 +105,14 @@ let rec betree_List_split_at
     | Betree_List_Nil -> Fail Failure
     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 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
   let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   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 *)
 let betree_List_pop_front
   (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
@@ -122,7 +122,7 @@ let betree_List_pop_front
   | Betree_List_Nil -> Fail Failure
   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 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
@@ -130,7 +130,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   | Betree_List_Nil -> Fail Failure
   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 *)
 let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
@@ -139,7 +139,7 @@ let betree_ListPairU64T_head_has_key
   | Betree_List_Nil -> Ok false
   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 *)
 let rec betree_ListPairU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
@@ -158,7 +158,7 @@ let rec betree_ListPairU64T_partition_at_pivot
   | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil)
   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 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
@@ -179,7 +179,7 @@ let betree_Leaf_split
   Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
     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 *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -203,7 +203,7 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   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 *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
@@ -219,7 +219,7 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Nil -> Ok None
   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 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
@@ -246,7 +246,7 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Ok (v, msgs1)
 
-(** [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 *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
@@ -261,7 +261,7 @@ let rec betree_Internal_lookup_in_children
     let* (st1, (o, n)) = betree_Node_lookup self.right key st in
     Ok (st1, (o, { self with right = n }))
 
-(** [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 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
@@ -317,7 +317,7 @@ and betree_Node_lookup
     Ok (st1, (o, Betree_Node_Leaf node))
   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 *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -337,7 +337,7 @@ let rec betree_Node_filter_messages_for_key
   | Betree_List_Nil -> Ok Betree_List_Nil
   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 *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -361,7 +361,7 @@ let rec betree_Node_lookup_first_message_after_key
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   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 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
@@ -421,7 +421,7 @@ let betree_Node_apply_to_internal
       betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
     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 *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
@@ -437,7 +437,7 @@ let rec betree_Node_apply_messages_to_internal
   | Betree_List_Nil -> Ok msgs
   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 *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
@@ -461,7 +461,7 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   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 *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
@@ -497,7 +497,7 @@ let betree_Node_apply_to_leaf
       lookup_mut_in_bindings_back bindings2
     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 *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
@@ -513,7 +513,7 @@ let rec betree_Node_apply_messages_to_leaf
   | Betree_List_Nil -> Ok bindings
   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 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
@@ -550,7 +550,7 @@ let rec betree_Internal_flush
     let (n, node_id_cnt1) = p1 in
     Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
 
-(** [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 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
@@ -591,7 +591,7 @@ and betree_Node_apply_messages
       Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   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 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
@@ -605,7 +605,7 @@ let betree_Node_apply
   let (self1, node_id_cnt1) = p in
   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 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
@@ -621,7 +621,7 @@ let betree_BeTree_new
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [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 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
@@ -632,7 +632,7 @@ let betree_BeTree_apply
   let (n, nic) = p in
   Ok (st1, { self with node_id_cnt = nic; root = n })
 
-(** [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 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
@@ -640,7 +640,7 @@ let betree_BeTree_insert
   =
   betree_BeTree_apply 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 *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) :
@@ -648,7 +648,7 @@ let betree_BeTree_delete
   =
   betree_BeTree_apply 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 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
@@ -657,7 +657,7 @@ let betree_BeTree_upsert
   =
   betree_BeTree_apply 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 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
@@ -666,11 +666,11 @@ let betree_BeTree_lookup
   let* (st1, (o, n)) = betree_Node_lookup self.root key st in
   Ok (st1, (o, { self with root = n }))
 
-(** [betree_main::main]:
+(** [betree::main]:
     Source: 'src/main.rs', lines 4:0-4:9 *)
 let main : result unit =
   Ok ()
 
-(** Unit test for [betree_main::main] *)
+(** Unit test for [betree::main] *)
 let _ = assert_norm (main = Ok ())
 
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/Betree.FunsExternal.fsti
index 8be98acf..db96eead 100644
--- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree/Betree.FunsExternal.fsti
@@ -1,29 +1,29 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-module BetreeMain.FunsExternal
+(** [betree]: external function declarations *)
+module Betree.FunsExternal
 open Primitives
-include BetreeMain.Types
+include Betree.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree_utils::load_internal_node]:
+(** [betree::betree_utils::load_internal_node]:
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 val 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 *)
 val betree_utils_store_internal_node
   :
   u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
     unit)
 
-(** [betree_main::betree_utils::load_leaf_node]:
+(** [betree::betree_utils::load_leaf_node]:
     Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 val 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 *)
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
diff --git a/tests/fstar/betree/BetreeMain.Types.fst b/tests/fstar/betree/Betree.Types.fst
index b87219b2..6b8e063b 100644
--- a/tests/fstar/betree/BetreeMain.Types.fst
+++ b/tests/fstar/betree/Betree.Types.fst
@@ -1,56 +1,56 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
+(** [betree]: type definitions *)
+module Betree.Types
 open Primitives
-include BetreeMain.TypesExternal
+include Betree.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::List]
+(** [betree::betree::List]
     Source: 'src/betree.rs', lines 17:0-17:23 *)
 type betree_List_t (t : Type0) =
 | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
 | Betree_List_Nil : betree_List_t t
 
-(** [betree_main::betree::UpsertFunState]
+(** [betree::betree::UpsertFunState]
     Source: 'src/betree.rs', lines 63:0-63:23 *)
 type 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 *)
 type betree_Message_t =
 | Betree_Message_Insert : u64 -> betree_Message_t
 | Betree_Message_Delete : 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 *)
 type betree_Leaf_t = { id : u64; size : u64; }
 
-(** [betree_main::betree::Internal]
+(** [betree::betree::Internal]
     Source: 'src/betree.rs', lines 156:0-156:15 *)
 type betree_Internal_t =
 {
   id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
 }
 
-(** [betree_main::betree::Node]
+(** [betree::betree::Node]
     Source: 'src/betree.rs', lines 179:0-179:9 *)
 and betree_Node_t =
 | Betree_Node_Internal : betree_Internal_t -> betree_Node_t
 | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
 
-(** [betree_main::betree::Params]
+(** [betree::betree::Params]
     Source: 'src/betree.rs', lines 187:0-187:13 *)
 type betree_Params_t = { min_flush_size : u64; split_size : u64; }
 
-(** [betree_main::betree::NodeIdCounter]
+(** [betree::betree::NodeIdCounter]
     Source: 'src/betree.rs', lines 201:0-201:20 *)
 type betree_NodeIdCounter_t = { next_node_id : u64; }
 
-(** [betree_main::betree::BeTree]
+(** [betree::betree::BeTree]
     Source: 'src/betree.rs', lines 218:0-218:17 *)
 type betree_BeTree_t =
 {
diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/Betree.TypesExternal.fsti
index 1b2c53a6..39e53ec9 100644
--- a/tests/fstar/betree/BetreeMain.TypesExternal.fsti
+++ b/tests/fstar/betree/Betree.TypesExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external type declarations *)
-module BetreeMain.TypesExternal
+(** [betree]: external type declarations *)
+module Betree.TypesExternal
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"