diff options
Diffstat (limited to 'tests/coq/hashmap_on_disk/HashmapMain_Opaque.v')
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Opaque.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 6152b94b..1ad9c697 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: opaque function definitions *) +(** [hashmap_main]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. @@ -8,12 +8,12 @@ Require Export HashmapMain_Types. Import HashmapMain_Types. Module HashmapMain_Opaque. -(** [hashmap_main::hashmap_utils::deserialize] *) +(** [hashmap_main::hashmap_utils::deserialize]: forward function *) Axiom hashmap_utils_deserialize_fwd : state -> result (state * (Hashmap_hash_map_t u64)) . -(** [hashmap_main::hashmap_utils::serialize] *) +(** [hashmap_main::hashmap_utils::serialize]: forward function *) Axiom hashmap_utils_serialize_fwd : Hashmap_hash_map_t u64 -> state -> result (state * unit) . |