summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v4
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v8
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject2
3 files changed, 4 insertions, 10 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0478edbe..ab424e42 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list
(T : Type) (n : nat) (ls : List_t T) (key : usize) :
result (T * (T -> result (List_t T)))
:=
- p <- hashMap_get_mut_in_list_loop T n ls key;
- let (t, back_'a) := p in
- Return (t, back_'a)
+ hashMap_get_mut_in_list_loop T n ls key
.
(** [hashmap::{hashmap::HashMap<T>}::get_mut]:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 6a7eeb2d..aff4995f 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -423,9 +423,7 @@ Definition hashmap_HashMap_get_mut_in_list
(T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) :
result (T * (T -> result (hashmap_List_t T)))
:=
- p <- hashmap_HashMap_get_mut_in_list_loop T n ls key;
- let (t, back_'a) := p in
- Return (t, back_'a)
+ hashmap_HashMap_get_mut_in_list_loop T n ls key
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
@@ -585,9 +583,7 @@ Definition insert_on_disk
p <- hashmap_utils_deserialize st;
let (st1, hm) := p in
hm1 <- hashmap_HashMap_insert u64 n hm key value;
- p1 <- hashmap_utils_serialize hm1 st1;
- let (st2, _) := p1 in
- Return (st2, tt)
+ hashmap_utils_serialize hm1 st1
.
(** [hashmap_main::main]:
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 41945494..d73541d9 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -4,9 +4,9 @@
-arg all
HashmapMain_Types.v
+HashmapMain_FunsExternal_Template.v
Primitives.v
HashmapMain_Funs.v
HashmapMain_TypesExternal.v
-HashmapMain_FunsExternal_Template.v
HashmapMain_FunsExternal.v
HashmapMain_TypesExternal_Template.v