diff options
| author | Aymeric Fromherz | 2024-05-31 14:25:23 +0200 |
|---|---|---|
| committer | Aymeric Fromherz | 2024-05-31 14:25:23 +0200 |
| commit | 2e3d1cdfde3e19af97e0d0fa47f92cfd66c688d9 (patch) | |
| tree | abd2aa08f32c9793ea6f32c4f8e16bee7e7a796d /tests/coq/hashmap | |
| parent | 2257d023478cd2fe44a0ff4d67c1c5b7e3b59061 (diff) | |
Regenerate tests
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 2 | ||||
| -rw-r--r-- | tests/coq/hashmap/_CoqProject | 4 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 2 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/_CoqProject | 12 |
4 files changed, 10 insertions, 10 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 6a4f8e99..1f2b2b22 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -211,7 +211,7 @@ Definition hashMap_move_elements_from_list Fixpoint hashMap_move_elements_loop (T : Type) (n : nat) (ntable : HashMap_t T) (slots : alloc_vec_Vec (List_t T)) (i : usize) : - result ((alloc_vec_Vec (List_t T)) * (HashMap_t T)) + result ((HashMap_t T) * (alloc_vec_Vec (List_t T))) := match n with | O => Fail_ OutOfFuel diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 7f80afbf..5d98662a 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg all -Hashmap_Types.v +Hashmap_Funs.v +Hashmap_Types.v Primitives.v -Hashmap_Funs.v diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index fd7f7f16..facd84ea 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -225,7 +225,7 @@ Definition hashmap_HashMap_move_elements_from_list Fixpoint hashmap_HashMap_move_elements_loop (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : - result ((alloc_vec_Vec (hashmap_List_t T)) * (hashmap_HashMap_t T)) + result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) := match n with | O => Fail_ OutOfFuel diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index d73541d9..837bbbaf 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -3,10 +3,10 @@ -arg -w -arg all -HashmapMain_Types.v -HashmapMain_FunsExternal_Template.v +HashmapMain_Funs.v +HashmapMain_FunsExternal.v +HashmapMain_FunsExternal_Template.v +HashmapMain_Types.v +HashmapMain_TypesExternal.v +HashmapMain_TypesExternal_Template.v Primitives.v -HashmapMain_Funs.v -HashmapMain_TypesExternal.v -HashmapMain_FunsExternal.v -HashmapMain_TypesExternal_Template.v |