From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/coq/betree/BetreeMain_Funs.v | 8 ++------
 tests/coq/betree/_CoqProject       | 2 +-
 2 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'tests/coq/betree')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3863a90f..a0338557 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -27,9 +27,7 @@ Definition betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_internal_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_internal_node id content st
 .
 
 (** [betree_main::betree::load_leaf_node]:
@@ -45,9 +43,7 @@ Definition betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_leaf_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_leaf_node id content st
 .
 
 (** [betree_main::betree::fresh_node_id]:
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 13e4b9c1..b14bed66 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,8 +3,8 @@
 -arg -w
 -arg all
 
-BetreeMain_Types.v
 BetreeMain_TypesExternal_Template.v
+BetreeMain_Types.v
 Primitives.v
 BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
-- 
cgit v1.2.3