Change the name of the generated Coq modules

5 files changed, 18 insertions, 18 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 .
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 .