From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Mar 2024 05:29:29 +0100 Subject: Regenerate the tests --- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 8 ++------ tests/coq/hashmap_on_disk/_CoqProject | 2 +- 2 files changed, 3 insertions(+), 7 deletions(-) (limited to 'tests/coq/hashmap_on_disk') 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}::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 -- cgit v1.2.3