diff options
Diffstat (limited to 'tests/coq/hashmap')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v (renamed from tests/coq/hashmap/Hashmap__Funs.v) | 8 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Types.v (renamed from tests/coq/hashmap/Hashmap__Types.v) | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tests/coq/hashmap/Hashmap__Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 7d897c8a..912b7fe2 100644 --- a/tests/coq/hashmap/Hashmap__Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -4,9 +4,9 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export Hashmap__Types. -Import Hashmap__Types. -Module Hashmap__Funs. +Require Export Hashmap_Types. +Import Hashmap_Types. +Module Hashmap_Funs. (** [hashmap::hash_key] *) Definition hash_key_fwd (k : usize) : result usize := Return k. @@ -538,4 +538,4 @@ Definition test1_fwd (n : nat) : result unit := end . -End Hashmap__Funs . +End Hashmap_Funs . diff --git a/tests/coq/hashmap/Hashmap__Types.v b/tests/coq/hashmap/Hashmap_Types.v index e1add060..a3b68f9a 100644 --- a/tests/coq/hashmap/Hashmap__Types.v +++ b/tests/coq/hashmap/Hashmap_Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module Hashmap__Types. +Module Hashmap_Types. (** [hashmap::List] *) Inductive List_t (T : Type) := @@ -35,4 +35,4 @@ Arguments Hash_map_slots {T}. Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. -End Hashmap__Types . +End Hashmap_Types . |