diff options
Diffstat (limited to 'tests/coq/betree/BetreeMain_Funs.v')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index ede82492..aadaa20d 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export BetreeMain_Types. -Import BetreeMain_Types. -Require Export BetreeMain_FunsExternal. -Import BetreeMain_FunsExternal. +Require Import BetreeMain_Types. +Include BetreeMain_Types. +Require Import BetreeMain_FunsExternal. +Include BetreeMain_FunsExternal. Module BetreeMain_Funs. (** [betree_main::betree::load_internal_node]: forward function @@ -1230,4 +1230,4 @@ Definition main : result unit := (** Unit test for [betree_main::main] *) Check (main )%return. -End BetreeMain_Funs . +End BetreeMain_Funs. |