From 5e38184af1b99a307271f738329cd96cb364fc1d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 22:31:48 +0200
Subject: Update the Makefile and regenerate the test files

---
 tests/coq/betree/BetreeMain_Funs.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tests/coq/betree/BetreeMain_Funs.v')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 86a9d5f2..85aecfc8 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export BetreeMain_Types.
 Import BetreeMain_Types.
@@ -1190,4 +1192,7 @@ Definition betree_be_tree_lookup_back
 Definition main_fwd : result unit :=
   Return tt.
 
+(** Unit test for [betree_main::main] *)
+Check (main_fwd )%return.
+
 End BetreeMain_Funs .
-- 
cgit v1.2.3