3 files changed, 12 insertions, 12 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 249adbe9..b4351dc3 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -4,11 +4,11 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain__Types.
-Import HashmapMain__Types.
-Require Export HashmapMain__Opaque.
-Import HashmapMain__Opaque.
-Module HashmapMain__Funs.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Require Export HashmapMain_Opaque.
+Import HashmapMain_Opaque.
+Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key] *)
 Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
@@ -595,4 +595,4 @@ Definition main_fwd : result unit := Return tt.
 (** Unit test for [hashmap_main::main] *)
 Check (main_fwd )%return.
 
-End HashmapMain__Funs .
+End HashmapMain_Funs .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
index 4b6db927..6152b94b 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -4,9 +4,9 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain__Types.
-Import HashmapMain__Types.
-Module HashmapMain__Opaque.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_Opaque.
 
 (** [hashmap_main::hashmap_utils::deserialize] *)
 Axiom hashmap_utils_deserialize_fwd
@@ -18,4 +18,4 @@ Axiom hashmap_utils_serialize_fwd
   : Hashmap_hash_map_t u64 -> state -> result (state * unit)
 .
 
-End HashmapMain__Opaque .
+End HashmapMain_Opaque .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index 5d609937..01243baf 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain__Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -4,7 +4,7 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Module HashmapMain__Types.
+Module HashmapMain_Types.
 
 (** [hashmap_main::hashmap::List] *)
 Inductive Hashmap_list_t (T : Type) :=
@@ -38,4 +38,4 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 (** The state type used in the state-error monad *)
 Axiom state : Type.
 
-End HashmapMain__Types .
+End HashmapMain_Types .