3 files changed, 12 insertions, 12 deletions
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 .