Regenerate the files

9 files changed, 98 insertions, 214 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index ddcff646..004db30e 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -15,9 +15,7 @@ Definition betree_load_internal_node_fwd
   (id : u64) (st : state) :
   result (state * (Betree_list_t (u64 * Betree_message_t)))
   :=
-  p <- betree_utils_load_internal_node_fwd id st;
-  let (st0, l) := p in
-  Return (st0, l)
+  betree_utils_load_internal_node_fwd id st
 .
 
 (** [betree_main::betree::store_internal_node] *)
@@ -33,9 +31,7 @@ Definition betree_store_internal_node_fwd
 (** [betree_main::betree::load_leaf_node] *)
 Definition betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) :=
-  p <- betree_utils_load_leaf_node_fwd id st;
-  let (st0, l) := p in
-  Return (st0, l)
+  betree_utils_load_leaf_node_fwd id st
 .
 
 (** [betree_main::betree::store_leaf_node] *)
@@ -55,7 +51,7 @@ Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
 
 (** [betree_main::betree::fresh_node_id] *)
 Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
-  counter0 <- u64_add counter 1%u64; Return counter0
+  u64_add counter 1%u64
 .
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
@@ -97,11 +93,9 @@ Definition betree_upsert_update_fwd
     match st with
     | BetreeUpsertFunStateAdd v =>
       margin <- u64_sub core_num_u64_max_c prev0;
-      if margin s>= v
-      then (i <- u64_add prev0 v; Return i)
-      else Return core_num_u64_max_c
+      if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
     | BetreeUpsertFunStateSub v =>
-      if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64)
+      if prev0 s>= v then u64_sub prev0 v else Return (0%u64)
     end
   end
 .
@@ -113,8 +107,7 @@ Fixpoint betree_list_len_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match self with
-    | BetreeListCons t tl =>
-      i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0
+    | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i
     | BetreeListNil => Return (0%u64)
     end
   end
@@ -258,8 +251,7 @@ Definition betree_leaf_split_back
   let (st0, _) := p1 in
   p2 <- betree_store_leaf_node_fwd id1 content1 st0;
   let (_, _) := p2 in
-  node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
-  Return node_id_cnt1
+  betree_node_id_counter_fresh_id_back node_id_cnt0
 .
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
@@ -278,7 +270,7 @@ Fixpoint betree_node_lookup_in_bindings_fwd
       else
         if i s> key
         then Return None
-        else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt)
+        else betree_node_lookup_in_bindings_fwd n0 key tl
     | BetreeListNil => Return None
     end
   end
@@ -297,9 +289,7 @@ Fixpoint betree_node_lookup_first_message_for_key_fwd
       let (i, m) := x in
       if i s>= key
       then Return (BetreeListCons (i, m) next_msgs)
-      else (
-        l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs;
-        Return l)
+      else betree_node_lookup_first_message_for_key_fwd n0 key next_msgs
     | BetreeListNil => Return BetreeListNil
     end
   end
@@ -348,9 +338,7 @@ Fixpoint betree_node_apply_upserts_fwd
       | BetreeMessageUpsert s =>
         v <- betree_upsert_update_fwd prev s;
         msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
-        p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st;
-        let (st0, i) := p in
-        Return (st0, i)
+        betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st
       end)
     else (
       p <- core_option_option_unwrap_fwd u64 prev st;
@@ -383,16 +371,13 @@ Fixpoint betree_node_apply_upserts_back
       | BetreeMessageUpsert s =>
         v <- betree_upsert_update_fwd prev s;
         msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
-        msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st;
-        Return msgs1
+        betree_node_apply_upserts_back n0 msgs0 (Some v) key st
       end)
     else (
       p <- core_option_option_unwrap_fwd u64 prev st;
       let (_, v) := p in
-      msgs0 <-
-        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
-          BetreeMessageInsert v);
-      Return msgs0)
+      betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
+        BetreeMessageInsert v))
   end
 .
 
@@ -556,14 +541,8 @@ with betree_internal_lookup_in_children_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     if key s< self.(Betree_internal_pivot)
-    then (
-      p <- betree_node_lookup_fwd n0 self.(Betree_internal_left) key st;
-      let (st0, opt) := p in
-      Return (st0, opt))
-    else (
-      p <- betree_node_lookup_fwd n0 self.(Betree_internal_right) key st;
-      let (st0, opt) := p in
-      Return (st0, opt))
+    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] *)
@@ -599,7 +578,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_fwd
       let (i, i0) := hd in
       if i s>= key
       then Return (BetreeListCons (i, i0) tl)
-      else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l)
+      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
     | BetreeListNil => Return BetreeListNil
     end
   end
@@ -643,43 +622,31 @@ Definition betree_node_apply_to_leaf_fwd_back
       bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
       bindings2 <-
         betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-      bindings3 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
-      Return bindings3
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
     | BetreeMessageDelete =>
       bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      bindings2 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
-      Return bindings2
+      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);
-      bindings3 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
-      Return bindings3
+      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);
-      bindings2 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
-      Return bindings2
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
     | BetreeMessageDelete =>
-      bindings1 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings0;
-      Return bindings1
+      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);
-      bindings2 <-
-        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
-      Return bindings2
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
     end
 .
 
@@ -696,9 +663,7 @@ Fixpoint betree_node_apply_messages_to_leaf_fwd_back
     | BetreeListCons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
-      bindings1 <-
-        betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl;
-      Return bindings1
+      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
     | BetreeListNil => Return bindings
     end
   end
@@ -720,8 +685,7 @@ Fixpoint betree_node_filter_messages_for_key_fwd_back
         msgs0 <-
           betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons
             (k, m) l);
-        msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
-        Return msgs1)
+        betree_node_filter_messages_for_key_fwd_back n0 key msgs0)
       else Return (BetreeListCons (k, m) l)
     | BetreeListNil => Return BetreeListNil
     end
@@ -740,9 +704,7 @@ Fixpoint betree_node_lookup_first_message_after_key_fwd
     | BetreeListCons p next_msgs =>
       let (k, m) := p in
       if k s= key
-      then (
-        l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs;
-        Return l)
+      then betree_node_lookup_first_message_after_key_fwd n0 key next_msgs
       else Return (BetreeListCons (k, m) next_msgs)
     | BetreeListNil => Return BetreeListNil
     end
@@ -788,15 +750,13 @@ Definition betree_node_apply_to_internal_fwd_back
       msgs2 <-
         betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
           BetreeMessageInsert i);
-      msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
-      Return msgs3
+      betree_node_lookup_first_message_for_key_back n key msgs msgs2
     | BetreeMessageDelete =>
       msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
       msgs2 <-
         betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
           BetreeMessageDelete);
-      msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
-      Return msgs3
+      betree_node_lookup_first_message_for_key_back n key msgs msgs2
     | BetreeMessageUpsert s =>
       p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0;
       let (_, m) := p in
@@ -807,18 +767,14 @@ Definition betree_node_apply_to_internal_fwd_back
         msgs2 <-
           betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
             BetreeMessageInsert v);
-        msgs3 <-
-          betree_node_lookup_first_message_for_key_back n key msgs msgs2;
-        Return msgs3
+        betree_node_lookup_first_message_for_key_back n key msgs msgs2
       | BetreeMessageDelete =>
         v <- betree_upsert_update_fwd None s;
         msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
         msgs2 <-
           betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
             BetreeMessageInsert v);
-        msgs3 <-
-          betree_node_lookup_first_message_for_key_back n key msgs msgs2;
-        Return msgs3
+        betree_node_lookup_first_message_for_key_back n key msgs msgs2
       | BetreeMessageUpsert ufs =>
         msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0;
         msgs2 <-
@@ -826,17 +782,14 @@ Definition betree_node_apply_to_internal_fwd_back
             BetreeMessageUpsert s);
         msgs3 <-
           betree_node_lookup_first_message_after_key_back n key msgs0 msgs2;
-        msgs4 <-
-          betree_node_lookup_first_message_for_key_back n key msgs msgs3;
-        Return msgs4
+        betree_node_lookup_first_message_for_key_back n key msgs msgs3
       end
     end
   else (
     msgs1 <-
       betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
         new_msg);
-    msgs2 <- betree_node_lookup_first_message_for_key_back n key msgs msgs1;
-    Return msgs2)
+    betree_node_lookup_first_message_for_key_back n key msgs msgs1)
 .
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
@@ -852,9 +805,7 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
     | BetreeListCons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m;
-      msgs1 <-
-        betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl;
-      Return msgs1
+      betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl
     | BetreeListNil => Return msgs
     end
   end
@@ -1101,11 +1052,8 @@ Definition betree_node_apply_back
   result (Betree_node_t * Betree_node_id_counter_t)
   :=
   let l := BetreeListNil in
-  p <-
-    betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st;
-  let (self0, node_id_cnt0) := p in
-  Return (self0, node_id_cnt0)
+  betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
+    (key, new_msg) l) st
 .
 
 (** [betree_main::betree::BeTree::{6}::new] *)
@@ -1169,8 +1117,7 @@ Definition betree_be_tree_insert_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result Betree_be_tree_t
   :=
-  self0 <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
-  Return self0
+  betree_be_tree_apply_back n self key (BetreeMessageInsert value) st
 .
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
@@ -1190,8 +1137,7 @@ Definition betree_be_tree_delete_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result Betree_be_tree_t
   :=
-  self0 <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
-  Return self0
+  betree_be_tree_apply_back n self key BetreeMessageDelete st
 .
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
@@ -1213,8 +1159,7 @@ Definition betree_be_tree_upsert_back
   (upd : Betree_upsert_fun_state_t) (st : state) :
   result Betree_be_tree_t
   :=
-  self0 <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
-  Return self0
+  betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st
 .
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
@@ -1222,9 +1167,7 @@ Definition betree_be_tree_lookup_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result (state * (option u64))
   :=
-  p <- betree_node_lookup_fwd n self.(Betree_be_tree_root) key st;
-  let (st0, opt) := p in
-  Return (st0, opt)
+  betree_node_lookup_fwd n self.(Betree_be_tree_root) key st
 .
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 17456d81..1ff3e576 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -24,8 +24,7 @@ Fixpoint hash_map_allocate_slots_fwd
     else (
       slots0 <- vec_push_back (List_t T) slots ListNil;
       i <- usize_sub n0 1%usize;
-      v <- hash_map_allocate_slots_fwd T n1 slots0 i;
-      Return v)
+      hash_map_allocate_slots_fwd T n1 slots0 i)
   end
 .
 
@@ -45,8 +44,7 @@ Definition hash_map_new_with_capacity_fwd
 
 (** [hashmap::HashMap::{0}::new] *)
 Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
-  hm <- hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize);
-  Return hm
+  hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
 .
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
@@ -62,8 +60,7 @@ Fixpoint hash_map_clear_slots_fwd_back
     then (
       slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
       i1 <- usize_add i 1%usize;
-      slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1;
-      Return slots1)
+      hash_map_clear_slots_fwd_back T n0 slots0 i1)
     else Return slots
   end
 .
@@ -93,7 +90,7 @@ Fixpoint hash_map_insert_in_list_fwd
     | ListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return false
-      else (b <- hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
+      else hash_map_insert_in_list_fwd T n0 key value ls0
     | ListNil => Return true
     end
   end
@@ -158,8 +155,7 @@ Fixpoint hash_map_move_elements_from_list_fwd_back
     match ls with
     | ListCons k v tl =>
       ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      ntable1 <- hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
-      Return ntable1
+      hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl
     | ListNil => Return ntable
     end
   end
@@ -183,9 +179,7 @@ Fixpoint hash_map_move_elements_fwd_back
       let l0 := mem_replace_back (List_t T) l ListNil in
       slots0 <- vec_index_mut_back (List_t T) slots i l0;
       i1 <- usize_add i 1%usize;
-      p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
-      let (ntable1, slots1) := p in
-      Return (ntable1, slots1))
+      hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1)
     else Return (ntable, slots)
   end
 .
@@ -221,7 +215,7 @@ Definition hash_map_insert_fwd_back
   self0 <- hash_map_insert_no_resize_fwd_back T n self key value;
   i <- hash_map_len_fwd T self0;
   if i s> self0.(Hash_map_max_load)
-  then (self1 <- hash_map_try_resize_fwd_back T n self0; Return self1)
+  then hash_map_try_resize_fwd_back T n self0
   else Return self0
 .
 
@@ -235,7 +229,7 @@ Fixpoint hash_map_contains_key_in_list_fwd
     | ListCons ckey t ls0 =>
       if ckey s= key
       then Return true
-      else (b <- hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
+      else hash_map_contains_key_in_list_fwd T n0 key ls0
     | ListNil => Return false
     end
   end
@@ -248,8 +242,7 @@ Definition hash_map_contains_key_fwd
   let i := vec_len (List_t T) self.(Hash_map_slots) in
   hash_mod <- usize_rem hash i;
   l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-  b <- hash_map_contains_key_in_list_fwd T n key l;
-  Return b
+  hash_map_contains_key_in_list_fwd T n key l
 .
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
@@ -262,7 +255,7 @@ Fixpoint hash_map_get_in_list_fwd
     | ListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return cvalue
-      else (t <- hash_map_get_in_list_fwd T n0 key ls0; Return t)
+      else hash_map_get_in_list_fwd T n0 key ls0
     | ListNil => Fail_ Failure
     end
   end
@@ -275,8 +268,7 @@ Definition hash_map_get_fwd
   let i := vec_len (List_t T) self.(Hash_map_slots) in
   hash_mod <- usize_rem hash i;
   l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-  t <- hash_map_get_in_list_fwd T n key l;
-  Return t
+  hash_map_get_in_list_fwd T n key l
 .
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -289,7 +281,7 @@ Fixpoint hash_map_get_mut_in_list_fwd
     | ListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return cvalue
-      else (t <- hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
+      else hash_map_get_mut_in_list_fwd T n0 key ls0
     | ListNil => Fail_ Failure
     end
   end
@@ -322,8 +314,7 @@ Definition hash_map_get_mut_fwd
   let i := vec_len (List_t T) self.(Hash_map_slots) in
   hash_mod <- usize_rem hash i;
   l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-  t <- hash_map_get_mut_in_list_fwd T n key l;
-  Return t
+  hash_map_get_mut_in_list_fwd T n key l
 .
 
 (** [hashmap::HashMap::{0}::get_mut] *)
@@ -356,7 +347,7 @@ Fixpoint hash_map_remove_from_list_fwd
         | ListCons i cvalue tl0 => Return (Some cvalue)
         | ListNil => Fail_ Failure
         end
-      else (opt <- hash_map_remove_from_list_fwd T n0 key tl; Return opt)
+      else hash_map_remove_from_list_fwd T n0 key tl
     | ListNil => Return None
     end
   end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 295ec489..3eaaec8a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -26,8 +26,7 @@ Fixpoint hashmap_hash_map_allocate_slots_fwd
     else (
       slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
       i <- usize_sub n0 1%usize;
-      v <- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i;
-      Return v)
+      hashmap_hash_map_allocate_slots_fwd T n1 slots0 i)
   end
 .
 
@@ -48,9 +47,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 Definition hashmap_hash_map_new_fwd
   (T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
-  hm <-
-    hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize);
-  Return hm
+  hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
@@ -66,8 +63,7 @@ Fixpoint hashmap_hash_map_clear_slots_fwd_back
     then (
       slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
       i1 <- usize_add i 1%usize;
-      slots1 <- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1;
-      Return slots1)
+      hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1)
     else Return slots
   end
 .
@@ -102,8 +98,7 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd
     | HashmapListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return false
-      else (
-        b <- hashmap_hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
+      else hashmap_hash_map_insert_in_list_fwd T n0 key value ls0
     | HashmapListNil => Return true
     end
   end
@@ -177,9 +172,7 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
     match ls with
     | HashmapListCons k v tl =>
       ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      ntable1 <-
-        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
-      Return ntable1
+      hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl
     | HashmapListNil => Return ntable
     end
   end
@@ -204,9 +197,7 @@ Fixpoint hashmap_hash_map_move_elements_fwd_back
       let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
       slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
       i1 <- usize_add i 1%usize;
-      p <- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
-      let (ntable1, slots1) := p in
-      Return (ntable1, slots1))
+      hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1)
     else Return (ntable, slots)
   end
 .
@@ -245,7 +236,7 @@ Definition hashmap_hash_map_insert_fwd_back
   self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n self key value;
   i <- hashmap_hash_map_len_fwd T self0;
   if i s> self0.(Hashmap_hash_map_max_load)
-  then (self1 <- hashmap_hash_map_try_resize_fwd_back T n self0; Return self1)
+  then hashmap_hash_map_try_resize_fwd_back T n self0
   else Return self0
 .
 
@@ -259,8 +250,7 @@ Fixpoint hashmap_hash_map_contains_key_in_list_fwd
     | HashmapListCons ckey t ls0 =>
       if ckey s= key
       then Return true
-      else (
-        b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
+      else hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0
     | HashmapListNil => Return false
     end
   end
@@ -275,8 +265,7 @@ Definition hashmap_hash_map_contains_key_fwd
   let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
   hash_mod <- usize_rem hash i;
   l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-  b <- hashmap_hash_map_contains_key_in_list_fwd T n key l;
-  Return b
+  hashmap_hash_map_contains_key_in_list_fwd T n key l
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
@@ -289,7 +278,7 @@ Fixpoint hashmap_hash_map_get_in_list_fwd
     | HashmapListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return cvalue
-      else (t <- hashmap_hash_map_get_in_list_fwd T n0 key ls0; Return t)
+      else hashmap_hash_map_get_in_list_fwd T n0 key ls0
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -304,8 +293,7 @@ Definition hashmap_hash_map_get_fwd
   let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
   hash_mod <- usize_rem hash i;
   l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-  t <- hashmap_hash_map_get_in_list_fwd T n key l;
-  Return t
+  hashmap_hash_map_get_in_list_fwd T n key l
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -318,7 +306,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_fwd
     | HashmapListCons ckey cvalue ls0 =>
       if ckey s= key
       then Return cvalue
-      else (t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
+      else hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -354,8 +342,7 @@ Definition hashmap_hash_map_get_mut_fwd
   hash_mod <- usize_rem hash i;
   l <-
     vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-  t <- hashmap_hash_map_get_mut_in_list_fwd T n key l;
-  Return t
+  hashmap_hash_map_get_mut_in_list_fwd T n key l
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
@@ -395,8 +382,7 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd
         | HashmapListCons i cvalue tl0 => Return (Some cvalue)
         | HashmapListNil => Fail_ Failure
         end
-      else (
-        opt <- hashmap_hash_map_remove_from_list_fwd T n0 key tl; Return opt)
+      else hashmap_hash_map_remove_from_list_fwd T n0 key tl
     | HashmapListNil => Return None
     end
   end
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 7d3e5a34..acc15a13 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -23,10 +23,10 @@ Definition x2_body : result u32 := Return (3%u32).
 Definition x2_c : u32 := x2_body%global.
 
 (** [constants::incr] *)
-Definition incr_fwd (n : u32) : result u32 := i <- u32_add n 1%u32; Return i.
+Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32.
 
 (** [constants::X3] *)
-Definition x3_body : result u32 := i <- incr_fwd (32%u32); Return i.
+Definition x3_body : result u32 := incr_fwd (32%u32).
 Definition x3_c : u32 := x3_body%global.
 
 (** [constants::mk_pair0] *)
@@ -47,15 +47,11 @@ Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
 .
 
 (** [constants::P0] *)
-Definition p0_body : result (u32 * u32) :=
-  p <- mk_pair0_fwd (0%u32) (1%u32); Return p
-.
+Definition p0_body : result (u32 * u32) := mk_pair0_fwd (0%u32) (1%u32).
 Definition p0_c : (u32 * u32) := p0_body%global.
 
 (** [constants::P1] *)
-Definition p1_body : result (Pair_t u32 u32) :=
-  p <- mk_pair1_fwd (0%u32) (1%u32); Return p
-.
+Definition p1_body : result (Pair_t u32 u32) := mk_pair1_fwd (0%u32) (1%u32).
 Definition p1_c : Pair_t u32 u32 := p1_body%global.
 
 (** [constants::P2] *)
@@ -80,16 +76,14 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
 .
 
 (** [constants::Y] *)
-Definition y_body : result (Wrap_t i32) :=
-  w <- wrap_new_fwd i32 (2%i32); Return w
-.
+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] *)
 Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val).
 
 (** [constants::YVAL] *)
-Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i.
+Definition yval_body : result i32 := unwrap_y_fwd.
 Definition yval_c : i32 := yval_body%global.
 
 (** [constants::get_z1::Z1] *)
@@ -100,9 +94,7 @@ Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
 Definition get_z1_fwd : result i32 := Return get_z1_z1_c.
 
 (** [constants::add] *)
-Definition add_fwd (a : i32) (b : i32) : result i32 :=
-  i <- i32_add a b; Return i
-.
+Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b.
 
 (** [constants::Q1] *)
 Definition q1_body : result i32 := Return (5%i32).
@@ -113,12 +105,12 @@ Definition q2_body : result i32 := Return q1_c.
 Definition q2_c : i32 := q2_body%global.
 
 (** [constants::Q3] *)
-Definition q3_body : result i32 := i <- add_fwd q2_c (3%i32); Return i.
+Definition q3_body : result i32 := add_fwd q2_c (3%i32).
 Definition q3_c : i32 := q3_body%global.
 
 (** [constants::get_z2] *)
 Definition get_z2_fwd : result i32 :=
-  i <- get_z1_fwd; i0 <- add_fwd i q3_c; i1 <- add_fwd q1_c i0; Return i1
+  i <- get_z1_fwd; i0 <- add_fwd i q3_c; add_fwd q1_c i0
 .
 
 (** [constants::S1] *)
@@ -126,7 +118,7 @@ Definition s1_body : result u32 := Return (6%u32).
 Definition s1_c : u32 := s1_body%global.
 
 (** [constants::S2] *)
-Definition s2_body : result u32 := i <- incr_fwd s1_c; Return i.
+Definition s2_body : result u32 := incr_fwd s1_c.
 Definition s2_c : u32 := s2_body%global.
 
 (** [constants::S3] *)
@@ -134,9 +126,7 @@ Definition s3_body : result (Pair_t u32 u32) := Return p3_c.
 Definition s3_c : Pair_t u32 u32 := s3_body%global.
 
 (** [constants::S4] *)
-Definition s4_body : result (Pair_t u32 u32) :=
-  p <- mk_pair1_fwd (7%u32) (8%u32); Return p
-.
+Definition s4_body : result (Pair_t u32 u32) := mk_pair1_fwd (7%u32) (8%u32).
 Definition s4_c : Pair_t u32 u32 := s4_body%global.
 
 End Constants .
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 3ddc1cf3..90390c1b 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -41,9 +41,7 @@ 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;
   let (st0, opt) := p in
-  p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0;
-  let (st1, nzu) := p0 in
-  Return (st1, nzu)
+  core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0
 .
 
 (** [external::test_vec] *)
@@ -94,10 +92,7 @@ Definition test_custom_swap_back
   (x : u32) (y : u32) (st : state) (st0 : state) :
   result (state * (u32 * u32))
   :=
-  p <- custom_swap_back u32 x y st (1%u32) st0;
-  let (st1, p0) := p in
-  let (x0, y0) := p0 in
-  Return (st1, (x0, y0))
+  custom_swap_back u32 x y st (1%u32) st0
 .
 
 (** [external::test_swap_non_zero] *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 48de76c2..b3f27546 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -25,10 +25,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd
     | ListCons x tl =>
       if i s= 0%u32
       then Return x
-      else (
-        i0 <- u32_sub i 1%u32;
-        t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
-        Return t)
+      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop0_fwd T n0 tl i0)
     | ListNil => Fail_ Failure
     end
   end
@@ -37,7 +34,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd
 (** [loops::list_nth_mut_loop] *)
 Definition list_nth_mut_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
+  list_nth_mut_loop_loop0_fwd T n ls i
 .
 
 (** [loops::list_nth_mut_loop] *)
@@ -66,7 +63,7 @@ Definition list_nth_mut_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
-  l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
+  list_nth_mut_loop_loop0_back T n ls i ret
 .
 
 End Loops .
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index a5f6126b..e91cf81a 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -46,37 +46,25 @@ Arguments SumLeft {T1} {T2} _.
 Arguments SumRight {T1} {T2} _.
 
 (** [no_nested_borrows::neg_test] *)
-Definition neg_test_fwd (x : i32) : result i32 := i <- i32_neg x; Return i.
+Definition neg_test_fwd (x : i32) : result i32 := i32_neg x.
 
 (** [no_nested_borrows::add_test] *)
-Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
-  i <- u32_add x y; Return i
-.
+Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y.
 
 (** [no_nested_borrows::subs_test] *)
-Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
-  i <- u32_sub x y; Return i
-.
+Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y.
 
 (** [no_nested_borrows::div_test] *)
-Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
-  i <- u32_div x y; Return i
-.
+Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y.
 
 (** [no_nested_borrows::div_test1] *)
-Definition div_test1_fwd (x : u32) : result u32 :=
-  i <- u32_div x 2%u32; Return i
-.
+Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32.
 
 (** [no_nested_borrows::rem_test] *)
-Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
-  i <- u32_rem x y; Return i
-.
+Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
 
 (** [no_nested_borrows::cast_test] *)
-Definition cast_test_fwd (x : u32) : result i32 :=
-  i <- scalar_cast U32 I32 x; Return i
-.
+Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
 
 (** [no_nested_borrows::test2] *)
 Definition test2_fwd : result unit :=
@@ -261,8 +249,7 @@ Arguments TreeNode {T} _ _ _.
 (** [no_nested_borrows::list_length] *)
 Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   match l with
-  | ListCons t l1 =>
-    i <- list_length_fwd T l1; i0 <- u32_add 1%u32 i; Return i0
+  | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i
   | ListNil => Return (0%u32)
   end
 .
@@ -273,7 +260,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0%u32
     then Return x
-    else (i0 <- u32_sub i 1%u32; t <- list_nth_shared_fwd T tl i0; Return t)
+    else (i0 <- u32_sub i 1%u32; list_nth_shared_fwd T tl i0)
   | ListNil => Fail_ Failure
   end
 .
@@ -284,7 +271,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0%u32
     then Return x
-    else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t)
+    else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0)
   | ListNil => Fail_ Failure
   end
 .
@@ -308,7 +295,7 @@ Fixpoint list_nth_mut_back
 Fixpoint list_rev_aux_fwd
   (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
   match li with
-  | ListCons hd tl => l <- list_rev_aux_fwd T tl (ListCons hd lo); Return l
+  | ListCons hd tl => list_rev_aux_fwd T tl (ListCons hd lo)
   | ListNil => Return lo
   end
 .
@@ -316,8 +303,7 @@ Fixpoint list_rev_aux_fwd
 (** [no_nested_borrows::list_rev] *)
 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
-  l0 <- list_rev_aux_fwd T li ListNil;
-  Return l0
+  list_rev_aux_fwd T li ListNil
 .
 
 (** [no_nested_borrows::test_list_functions] *)
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 616eed37..cb4486c6 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -7,9 +7,7 @@ Local Open Scope Primitives_scope.
 Module Paper.
 
 (** [paper::ref_incr] *)
-Definition ref_incr_fwd_back (x : i32) : result i32 :=
-  x0 <- i32_add x 1%i32; Return x0
-.
+Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32.
 
 (** [paper::test_incr] *)
 Definition test_incr_fwd : result unit :=
@@ -63,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0%u32
     then Return x
-    else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t)
+    else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0)
   | ListNil => Fail_ Failure
   end
 .
@@ -86,7 +84,7 @@ Fixpoint list_nth_mut_back
 (** [paper::sum] *)
 Fixpoint sum_fwd (l : List_t i32) : result i32 :=
   match l with
-  | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0
+  | ListCons x tl => i <- sum_fwd tl; i32_add x i
   | ListNil => Return (0%i32)
   end
 .
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index a45c77c5..bd6df02e 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -19,9 +19,7 @@ Arguments ListNil {T}.
 Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) :=
   match ls with
   | ListCons hd tl =>
-    if hd s= x
-    then Return (ListCons hd tl)
-    else (l <- get_list_at_x_fwd tl x; Return l)
+    if hd s= x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
   | ListNil => Return ListNil
   end
 .