From 2e3d1cdfde3e19af97e0d0fa47f92cfd66c688d9 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 14:25:23 +0200
Subject: Regenerate tests

---
 tests/coq/arrays/_CoqProject                 |  2 +-
 tests/coq/betree/_CoqProject                 | 12 ++++++------
 tests/coq/demo/_CoqProject                   |  2 +-
 tests/coq/hashmap/Hashmap_Funs.v             |  2 +-
 tests/coq/hashmap/_CoqProject                |  4 ++--
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v |  2 +-
 tests/coq/hashmap_on_disk/_CoqProject        | 12 ++++++------
 tests/coq/misc/_CoqProject                   | 24 ++++++++++++------------
 tests/coq/traits/_CoqProject                 |  2 +-
 9 files changed, 31 insertions(+), 31 deletions(-)

(limited to 'tests/coq')

diff --git a/tests/coq/arrays/_CoqProject b/tests/coq/arrays/_CoqProject
index a4e82408..4ccc7663 100644
--- a/tests/coq/arrays/_CoqProject
+++ b/tests/coq/arrays/_CoqProject
@@ -3,5 +3,5 @@
 -arg -w
 -arg all
 
-Arrays.v
+Arrays.v 
 Primitives.v
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index b14bed66..2ba444c2 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,10 +3,10 @@
 -arg -w
 -arg all
 
-BetreeMain_TypesExternal_Template.v
-BetreeMain_Types.v
+BetreeMain_Funs.v 
+BetreeMain_FunsExternal.v 
+BetreeMain_FunsExternal_Template.v 
+BetreeMain_Types.v 
+BetreeMain_TypesExternal.v 
+BetreeMain_TypesExternal_Template.v 
 Primitives.v
-BetreeMain_FunsExternal_Template.v
-BetreeMain_Funs.v
-BetreeMain_TypesExternal.v
-BetreeMain_FunsExternal.v
diff --git a/tests/coq/demo/_CoqProject b/tests/coq/demo/_CoqProject
index 62554699..67e4f2a4 100644
--- a/tests/coq/demo/_CoqProject
+++ b/tests/coq/demo/_CoqProject
@@ -3,5 +3,5 @@
 -arg -w
 -arg all
 
-Demo.v
+Demo.v 
 Primitives.v
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
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 308de4f4..bffb6699 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,16 +3,16 @@
 -arg -w
 -arg all
 
-External_FunsExternal_Template.v
-Loops.v
-External_Types.v
+Bitwise.v 
+Constants.v 
+External_Funs.v 
+External_FunsExternal.v 
+External_FunsExternal_Template.v 
+External_Types.v 
+External_TypesExternal.v 
+External_TypesExternal_Template.v 
+Loops.v 
+NoNestedBorrows.v 
+Paper.v 
+PoloniusList.v 
 Primitives.v
-External_Funs.v
-External_TypesExternal.v
-Constants.v
-PoloniusList.v
-NoNestedBorrows.v
-External_FunsExternal.v
-Bitwise.v
-External_TypesExternal_Template.v
-Paper.v
diff --git a/tests/coq/traits/_CoqProject b/tests/coq/traits/_CoqProject
index 5b6199fc..14a91aa8 100644
--- a/tests/coq/traits/_CoqProject
+++ b/tests/coq/traits/_CoqProject
@@ -3,5 +3,5 @@
 -arg -w
 -arg all
 
+Primitives.v 
 Traits.v
-Primitives.v
-- 
cgit v1.2.3