Merge pull request #33 from AeneasVerif/son_refactor

Update the code following Charon's refactor

3 files changed, 273 insertions, 273 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 85aecfc8..e15085ff 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -260,28 +260,6 @@ Definition betree_leaf_split_back
   betree_node_id_counter_fresh_id_back node_id_cnt0
 .
 
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s= key
-      then Return (Some i0)
-      else
-        if i s> key
-        then Return None
-        else betree_node_lookup_in_bindings_fwd n0 key tl
-    | BetreeListNil => Return None
-    end
-  end
-.
-
 (** [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)) :
@@ -386,8 +364,62 @@ Fixpoint betree_node_apply_upserts_back
   end
 .
 
+(** [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)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match bindings with
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s= key
+      then Return (Some i0)
+      else
+        if i s> key
+        then Return None
+        else betree_node_lookup_in_bindings_fwd n0 key tl
+    | BetreeListNil => Return None
+    end
+  end
+.
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+Fixpoint betree_internal_lookup_in_children_fwd
+  (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
+  result (state * (option u64))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    if key s< self.(Betree_internal_pivot)
+    then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
+    else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
+  end
+
+(** [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
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    if key s< self.(Betree_internal_pivot)
+    then (
+      n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
+    else (
+      n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
+  end
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-Fixpoint betree_node_lookup_fwd
+with betree_node_lookup_fwd
   (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
   result (state * (option u64))
   :=
@@ -526,144 +558,6 @@ with betree_node_lookup_back
       Return (BetreeNodeLeaf node)
     end
   end
-
-(** [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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    if key s< self.(Betree_internal_pivot)
-    then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
-    else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
-  end
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    if key s< self.(Betree_internal_pivot)
-    then (
-      n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
-      Return (mkBetree_internal_t self.(Betree_internal_id)
-        self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
-    else (
-      n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
-      Return (mkBetree_internal_t self.(Betree_internal_id)
-        self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
-  end
-.
-
-(** [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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s>= key
-      then Return (BetreeListCons (i, i0) tl)
-      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
-    | BetreeListNil => Return BetreeListNil
-    end
-  end
-.
-
-(** [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)) :
-  result (Betree_list_t (u64 * u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s>= key
-      then Return ret
-      else (
-        tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
-        Return (BetreeListCons (i, i0) tl0))
-    | BetreeListNil => Return ret
-    end
-  end
-.
-
-(** [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) :
-  result (Betree_list_t (u64 * u64))
-  :=
-  bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
-  b <- betree_list_head_has_key_fwd u64 bindings0 key;
-  if b
-  then (
-    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
-    match new_msg with
-    | BetreeMessageInsert v =>
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      bindings2 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
-    | BetreeMessageDelete =>
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    | BetreeMessageUpsert s =>
-      let (_, i) := hd in
-      v <- betree_upsert_update_fwd (Some i) s;
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      bindings2 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
-    end)
-  else
-    match new_msg with
-    | BetreeMessageInsert v =>
-      bindings1 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    | BetreeMessageDelete =>
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings0
-    | BetreeMessageUpsert s =>
-      v <- betree_upsert_update_fwd None s;
-      bindings1 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    end
-.
-
-(** [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)) :
-  result (Betree_list_t (u64 * u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match new_msgs with
-    | BetreeListCons new_msg new_msgs_tl =>
-      let (i, m) := new_msg in
-      bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
-      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
-    | BetreeListNil => Return bindings
-    end
-  end
 .
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
@@ -811,8 +705,210 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
   end
 .
 
+(** [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))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match bindings with
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s>= key
+      then Return (BetreeListCons (i, i0) tl)
+      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
+    | BetreeListNil => Return BetreeListNil
+    end
+  end
+.
+
+(** [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)) :
+  result (Betree_list_t (u64 * u64))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match bindings with
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s>= key
+      then Return ret
+      else (
+        tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
+        Return (BetreeListCons (i, i0) tl0))
+    | BetreeListNil => Return ret
+    end
+  end
+.
+
+(** [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) :
+  result (Betree_list_t (u64 * u64))
+  :=
+  bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
+  b <- betree_list_head_has_key_fwd u64 bindings0 key;
+  if b
+  then (
+    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+    | BetreeMessageDelete =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    | BetreeMessageUpsert s =>
+      let (_, i) := hd in
+      v <- betree_upsert_update_fwd (Some i) s;
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+    end)
+  else
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    | BetreeMessageDelete =>
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings0
+    | BetreeMessageUpsert s =>
+      v <- betree_upsert_update_fwd None s;
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    end
+.
+
+(** [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)) :
+  result (Betree_list_t (u64 * u64))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match new_msgs with
+    | BetreeListCons new_msg new_msgs_tl =>
+      let (i, m) := new_msg in
+      bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
+      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
+    | BetreeListNil => Return bindings
+    end
+  end
+.
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+Fixpoint betree_internal_flush_fwd
+  (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
+  (node_id_cnt : Betree_node_id_counter_t)
+  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
+  result (state * (Betree_list_t (u64 * Betree_message_t)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    p <-
+      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (st0, _) := p0 in
+      p1 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (_, node_id_cnt0) := p1 in
+      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+      if len_right s>= params.(Betree_params_min_flush_size)
+      then (
+        p2 <-
+          betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+            node_id_cnt0 msgs_right st0;
+        let (st1, _) := p2 in
+        _ <-
+          betree_node_apply_messages_back n0 self.(Betree_internal_right)
+            params node_id_cnt0 msgs_right st0;
+        Return (st1, BetreeListNil))
+      else Return (st0, msgs_right))
+    else (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      let (st0, _) := p0 in
+      _ <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      Return (st0, msgs_left))
+  end
+
+(** [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)
+  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
+  result (Betree_internal_t * Betree_node_id_counter_t)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    p <-
+      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (st0, _) := p0 in
+      p1 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (n1, node_id_cnt0) := p1 in
+      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+      if len_right s>= params.(Betree_params_min_flush_size)
+      then (
+        p2 <-
+          betree_node_apply_messages_back n0 self.(Betree_internal_right)
+            params node_id_cnt0 msgs_right st0;
+        let (n2, node_id_cnt1) := p2 in
+        Return (mkBetree_internal_t self.(Betree_internal_id)
+          self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
+      else
+        Return (mkBetree_internal_t self.(Betree_internal_id)
+          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
+          node_id_cnt0))
+    else (
+      p0 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      let (n1, node_id_cnt0) := p0 in
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
+        node_id_cnt0))
+  end
+
 (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-Fixpoint betree_node_apply_messages_fwd
+with betree_node_apply_messages_fwd
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
   (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) :
@@ -922,102 +1018,6 @@ with betree_node_apply_messages_back
           |}, node_id_cnt))
     end
   end
-
-(** [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)
-  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
-  result (state * (Betree_list_t (u64 * Betree_message_t)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
-        self.(Betree_internal_pivot);
-    let (msgs_left, msgs_right) := p in
-    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-    if len_left s>= params.(Betree_params_min_flush_size)
-    then (
-      p0 <-
-        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
-          node_id_cnt msgs_left st;
-      let (st0, _) := p0 in
-      p1 <-
-        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
-          node_id_cnt msgs_left st;
-      let (_, node_id_cnt0) := p1 in
-      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
-      if len_right s>= params.(Betree_params_min_flush_size)
-      then (
-        p2 <-
-          betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
-            node_id_cnt0 msgs_right st0;
-        let (st1, _) := p2 in
-        _ <-
-          betree_node_apply_messages_back n0 self.(Betree_internal_right)
-            params node_id_cnt0 msgs_right st0;
-        Return (st1, BetreeListNil))
-      else Return (st0, msgs_right))
-    else (
-      p0 <-
-        betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
-          node_id_cnt msgs_right st;
-      let (st0, _) := p0 in
-      _ <-
-        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
-          node_id_cnt msgs_right st;
-      Return (st0, msgs_left))
-  end
-
-(** [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)
-  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
-  result (Betree_internal_t * Betree_node_id_counter_t)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
-        self.(Betree_internal_pivot);
-    let (msgs_left, msgs_right) := p in
-    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-    if len_left s>= params.(Betree_params_min_flush_size)
-    then (
-      p0 <-
-        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
-          node_id_cnt msgs_left st;
-      let (st0, _) := p0 in
-      p1 <-
-        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
-          node_id_cnt msgs_left st;
-      let (n1, node_id_cnt0) := p1 in
-      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
-      if len_right s>= params.(Betree_params_min_flush_size)
-      then (
-        p2 <-
-          betree_node_apply_messages_back n0 self.(Betree_internal_right)
-            params node_id_cnt0 msgs_right st0;
-        let (n2, node_id_cnt1) := p2 in
-        Return (mkBetree_internal_t self.(Betree_internal_id)
-          self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
-      else
-        Return (mkBetree_internal_t self.(Betree_internal_id)
-          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
-          node_id_cnt0))
-    else (
-      p0 <-
-        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
-          node_id_cnt msgs_right st;
-      let (n1, node_id_cnt0) := p0 in
-      Return (mkBetree_internal_t self.(Betree_internal_id)
-        self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
-        node_id_cnt0))
-  end
 .
 
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index c8af54cd..4a4e75aa 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -37,19 +37,19 @@ mkBetree_leaf_t {
 }
 .
 
-(** [betree_main::betree::Node] *)
-Inductive Betree_node_t :=
-| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
-| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
-
 (** [betree_main::betree::Internal] *)
-with Betree_internal_t :=
+Inductive Betree_internal_t :=
 | mkBetree_internal_t :
   u64 ->
   u64 ->
   Betree_node_t ->
   Betree_node_t ->
   Betree_internal_t
+
+(** [betree_main::betree::Node] *)
+with Betree_node_t :=
+| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
+| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
 .
 
 Definition Betree_internal_id (x : Betree_internal_t) :=
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index f93254e1..c1c24e00 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -238,23 +238,23 @@ Definition test_char_fwd : result char :=
   Return (char_of_byte Coq.Init.Byte.x61)
 .
 
-(** [no_nested_borrows::NodeElem] *)
-Inductive Node_elem_t (T : Type) :=
-| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
-| NodeElemNil : Node_elem_t T
-
 (** [no_nested_borrows::Tree] *)
-with Tree_t (T : Type) :=
+Inductive Tree_t (T : Type) :=
 | TreeLeaf : T -> Tree_t T
 | TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T
-.
 
-Arguments NodeElemCons {T} _ _.
-Arguments NodeElemNil {T}.
+(** [no_nested_borrows::NodeElem] *)
+with Node_elem_t (T : Type) :=
+| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
+| NodeElemNil : Node_elem_t T
+.
 
 Arguments TreeLeaf {T} _.
 Arguments TreeNode {T} _ _ _.
 
+Arguments NodeElemCons {T} _ _.
+Arguments NodeElemNil {T}.
+
 (** [no_nested_borrows::list_length]: forward function *)
 Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   match l with