summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
authorSon Ho2023-11-09 16:24:07 +0100
committerSon Ho2023-11-09 16:24:07 +0100
commit49ffc966cfdbd71f8c83a3c72ab81e1bb101f420 (patch)
treea60e31612f0049a7b3d1c2e616b3f18c230f7f82 /tests/coq/hashmap
parent3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 (diff)
Regenerate the Coq test files
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Types.v14
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Types.v14
2 files changed, 14 insertions, 14 deletions
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index 63d30eeb..8529803d 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -14,8 +14,8 @@ Inductive List_t (T : Type) :=
| List_Nil : List_t T
.
-Arguments List_Cons {T} _ _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [hashmap::HashMap] *)
Record HashMap_t (T : Type) :=
@@ -27,10 +27,10 @@ mkHashMap_t {
}
.
-Arguments mkHashMap_t {T} _ _ _ _.
-Arguments hashMap_num_entries {T}.
-Arguments hashMap_max_load_factor {T}.
-Arguments hashMap_max_load {T}.
-Arguments hashMap_slots {T}.
+Arguments mkHashMap_t { _ }.
+Arguments hashMap_num_entries { _ }.
+Arguments hashMap_max_load_factor { _ }.
+Arguments hashMap_max_load { _ }.
+Arguments hashMap_slots { _ }.
End Hashmap_Types .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index 466119f8..95e5f35b 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -14,8 +14,8 @@ Inductive hashmap_List_t (T : Type) :=
| Hashmap_List_Nil : hashmap_List_t T
.
-Arguments Hashmap_List_Cons {T} _ _ _.
-Arguments Hashmap_List_Nil {T}.
+Arguments Hashmap_List_Cons { _ }.
+Arguments Hashmap_List_Nil { _ }.
(** [hashmap_main::hashmap::HashMap] *)
Record hashmap_HashMap_t (T : Type) :=
@@ -27,11 +27,11 @@ mkhashmap_HashMap_t {
}
.
-Arguments mkhashmap_HashMap_t {T} _ _ _ _.
-Arguments hashmap_HashMap_num_entries {T}.
-Arguments hashmap_HashMap_max_load_factor {T}.
-Arguments hashmap_HashMap_max_load {T}.
-Arguments hashmap_HashMap_slots {T}.
+Arguments mkhashmap_HashMap_t { _ }.
+Arguments hashmap_HashMap_num_entries { _ }.
+Arguments hashmap_HashMap_max_load_factor { _ }.
+Arguments hashmap_HashMap_max_load { _ }.
+Arguments hashmap_HashMap_slots { _ }.
(** The state type used in the state-error monad *)
Axiom state : Type.