summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Translate.ml2
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v (renamed from tests/coq/betree/BetreeMain__Funs.v)12
-rw-r--r--tests/coq/betree/BetreeMain_Opaque.v (renamed from tests/coq/betree/BetreeMain__Opaque.v)8
-rw-r--r--tests/coq/betree/BetreeMain_Types.v (renamed from tests/coq/betree/BetreeMain__Types.v)4
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v (renamed from tests/coq/hashmap/Hashmap__Funs.v)8
-rw-r--r--tests/coq/hashmap/Hashmap_Types.v (renamed from tests/coq/hashmap/Hashmap__Types.v)4
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Funs.v)12
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Opaque.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Opaque.v)8
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Types.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Types.v)4
-rw-r--r--tests/coq/misc/External_Funs.v (renamed from tests/coq/misc/External__Funs.v)12
-rw-r--r--tests/coq/misc/External_Opaque.v (renamed from tests/coq/misc/External__Opaque.v)8
-rw-r--r--tests/coq/misc/External_Types.v (renamed from tests/coq/misc/External__Types.v)4
12 files changed, 43 insertions, 43 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 012669dc..f34231e0 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -752,7 +752,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
in
let module_delimiter =
- match !Config.backend with FStar -> "." | Coq -> "__"
+ match !Config.backend with FStar -> "." | Coq -> "_"
in
(* Extract one or several files, depending on the configuration *)
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 .
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 01:34:25 +0000