Change the name of the generated Coq modules

11 files changed, 42 insertions, 42 deletions

diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3ce86f6b..3129614c 100644
--- a/tests/coq/betree/BetreeMain__Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -4,11 +4,11 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain__Types.
-Import BetreeMain__Types.
-Require Export BetreeMain__Opaque.
-Import BetreeMain__Opaque.
-Module BetreeMain__Funs.
+Require Export BetreeMain_Types.
+Import BetreeMain_Types.
+Require Export BetreeMain_Opaque.
+Import BetreeMain_Opaque.
+Module BetreeMain_Funs.
 
 (** [betree_main::betree::load_internal_node] *)
 Definition betree_load_internal_node_fwd
@@ -1394,4 +1394,4 @@ Definition betree_be_tree_lookup_back
 (** [betree_main::main] *)
 Definition main_fwd : result unit := Return tt.
 
-End BetreeMain__Funs .
+End BetreeMain_Funs .
diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index cbd8cfb3..08ab530a 100644
--- a/tests/coq/betree/BetreeMain__Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -4,9 +4,9 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain__Types.
-Import BetreeMain__Types.
-Module BetreeMain__Opaque.
+Require Export BetreeMain_Types.
+Import BetreeMain_Types.
+Module BetreeMain_Opaque.
 
 (** [betree_main::betree_utils::load_internal_node] *)
 Axiom betree_utils_load_internal_node_fwd
@@ -35,4 +35,4 @@ Axiom core_option_option_unwrap_fwd :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End BetreeMain__Opaque .
+End BetreeMain_Opaque .
diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain_Types.v
index 2ed0d324..672b2ebd 100644
--- a/tests/coq/betree/BetreeMain__Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -4,7 +4,7 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Module BetreeMain__Types.
+Module BetreeMain_Types.
 
 (** [betree_main::betree::List] *)
 Inductive Betree_list_t (T : Type) :=
@@ -82,4 +82,4 @@ Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
 (** The state type used in the state-error monad *)
 Axiom state : Type.
 
-End BetreeMain__Types .
+End BetreeMain_Types .
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 .
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External_Funs.v
index e7020040..3ddc1cf3 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -4,11 +4,11 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export External__Types.
-Import External__Types.
-Require Export External__Opaque.
-Import External__Opaque.
-Module External__Funs.
+Require Export External_Types.
+Import External_Types.
+Require Export External_Opaque.
+Import External_Opaque.
+Module External_Funs.
 
 (** [external::swap] *)
 Definition swap_fwd
@@ -111,4 +111,4 @@ Definition test_swap_non_zero_fwd
   if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
 .
 
-End External__Funs .
+End External_Funs .
diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External_Opaque.v
index 93652450..d60251e0 100644
--- a/tests/coq/misc/External__Opaque.v
+++ b/tests/coq/misc/External_Opaque.v
@@ -4,9 +4,9 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export External__Types.
-Import External__Types.
-Module External__Opaque.
+Require Export External_Types.
+Import External_Types.
+Module External_Opaque.
 
 (** [core::mem::swap] *)
 Axiom core_mem_swap_fwd :
@@ -33,4 +33,4 @@ Axiom core_option_option_unwrap_fwd :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End External__Opaque .
+End External_Opaque .
diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External_Types.v
index f4f74272..cec5b88e 100644
--- a/tests/coq/misc/External__Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -4,7 +4,7 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Module External__Types.
+Module External_Types.
 
 (** [core::num::nonzero::NonZeroU32] *)
 Axiom Core_num_nonzero_non_zero_u32_t : Type.
@@ -12,4 +12,4 @@ Axiom Core_num_nonzero_non_zero_u32_t : Type.
 (** The state type used in the state-error monad *)
 Axiom state : Type.
 
-End External__Types .
+End External_Types .