diff options
| author | Son Ho | 2024-03-19 05:29:29 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-19 05:29:29 +0100 |
| commit | f3e16bb43a8ff27a5184d9fa452277cc6a59410f (patch) | |
| tree | f79760b40b3a9f404b1db0d61f9d452408ef1de5 /tests/coq/betree | |
| parent | 5a1373f5492f65ff0da6f7e0c34b056a98070908 (diff) | |
Regenerate the tests
Diffstat (limited to 'tests/coq/betree')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 8 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 2 |
2 files changed, 3 insertions, 7 deletions
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 |