From 8ac12ccdd3e55b8da910c6c8b7bb8dff94a6a640 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 Jan 2023 19:18:18 +0100
Subject: Regenerate the hashmap code and update the proofs

---
 tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/fstar/betree_back_stateful')

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index c06a6b9e..01fc457e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -272,7 +272,7 @@ let betree_leaf_split_back0
             | Return (st1, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st1 with
               | Fail e -> Fail e
-              | Return (_, _) -> Return (st0, ())
+              | Return _ -> Return (st0, ())
               end
             end
           end
-- 
cgit v1.2.3