Change the name of the generated Coq modules

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 .