summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap_on_disk
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/hashmap_on_disk')
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v10
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v6
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Types.v7
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v15
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v15
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject2
6 files changed, 43 insertions, 12 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 188c98b3..faba0afe 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
-Require Export HashmapMain_FunsExternal.
-Import HashmapMain_FunsExternal.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
+Require Import HashmapMain_FunsExternal.
+Include HashmapMain_FunsExternal.
Module HashmapMain_Funs.
(** [hashmap_main::hashmap::hash_key]: forward function
@@ -717,4 +717,4 @@ Definition insert_on_disk
Definition main : result unit :=
Return tt.
-End HashmapMain_Funs .
+End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
index b5a4a101..e10d02f6 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
Module HashmapMain_FunsExternal_Template.
(** [hashmap_main::hashmap_utils::deserialize]: forward function
@@ -23,4 +23,4 @@ Axiom hashmap_utils_serialize
: hashmap_HashMap_t u64 -> state -> result (state * unit)
.
-End HashmapMain_FunsExternal_Template .
+End HashmapMain_FunsExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index 039b7e72..8d3d72aa 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
+Require Import HashmapMain_TypesExternal.
+Include HashmapMain_TypesExternal.
Module HashmapMain_Types.
(** [hashmap_main::hashmap::List]
@@ -35,7 +37,4 @@ Arguments hashmap_HashMap_max_load_factor { _ }.
Arguments hashmap_HashMap_max_load { _ }.
Arguments hashmap_HashMap_slots { _ }.
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End HashmapMain_Types .
+End HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
new file mode 100644
index 00000000..87568232
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
new file mode 100644
index 00000000..391b2775
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal_Template.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index a85fa1fe..41945494 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,5 +6,7 @@
HashmapMain_Types.v
Primitives.v
HashmapMain_Funs.v
+HashmapMain_TypesExternal.v
HashmapMain_FunsExternal_Template.v
HashmapMain_FunsExternal.v
+HashmapMain_TypesExternal_Template.v