From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 09:37:31 +0100 Subject: Update the generation of files for external definitions and regenerate the tests --- tests/coq/betree/BetreeMain_Funs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (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 8e48b17d..ede82492 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -8,8 +8,8 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export BetreeMain_Types. Import BetreeMain_Types. -Require Export BetreeMain_Opaque. -Import BetreeMain_Opaque. +Require Export BetreeMain_FunsExternal. +Import BetreeMain_FunsExternal. Module BetreeMain_Funs. (** [betree_main::betree::load_internal_node]: forward function -- cgit v1.2.3 From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 10:29:25 +0100 Subject: Generate a dedicated file for the external types --- tests/coq/betree/BetreeMain_Funs.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (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 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. -- cgit v1.2.3