13 files changed, 35 insertions, 35 deletions
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
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 38be12ac..2aca9fbe 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -158,7 +158,7 @@ let hashMap_move_elements_from_list
 let rec hashMap_move_elements_loop
   (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t))
   (i : usize) :
-  Tot (result ((alloc_vec_Vec (list_t t)) & (hashMap_t t)))
+  Tot (result ((hashMap_t t) & (alloc_vec_Vec (list_t t))))
   (decreases (hashMap_move_elements_loop_decreases t ntable slots i))
   =
   let i1 = alloc_vec_Vec_len (list_t t) slots in
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index cf3ae858..4a032207 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -167,7 +167,7 @@ let hashmap_HashMap_move_elements_from_list
 let rec hashmap_HashMap_move_elements_loop
   (t : Type0) (ntable : hashmap_HashMap_t t)
   (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) :
-  Tot (result ((alloc_vec_Vec (hashmap_List_t t)) & (hashmap_HashMap_t t)))
+  Tot (result ((hashmap_HashMap_t t) & (alloc_vec_Vec (hashmap_List_t t))))
   (decreases (hashmap_HashMap_move_elements_loop_decreases t ntable slots i))
   =
   let i1 = alloc_vec_Vec_len (hashmap_List_t t) slots in
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 17ad26f7..cb11e5cf 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -157,7 +157,7 @@ def HashMap.move_elements_from_list
 divergent def HashMap.move_elements_loop
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize)
   :
-  Result ((alloc.vec.Vec (List T)) × (HashMap T))
+  Result ((HashMap T) × (alloc.vec.Vec (List T)))
   :=
   let i1 := alloc.vec.Vec.len (List T) slots
   if i < i1
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 56039741..e27305b1 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -167,7 +167,7 @@ def hashmap.HashMap.move_elements_from_list
 divergent def hashmap.HashMap.move_elements_loop
   (T : Type) (ntable : hashmap.HashMap T)
   (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
-  Result ((alloc.vec.Vec (hashmap.List T)) × (hashmap.HashMap T))
+  Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
   :=
   let i1 := alloc.vec.Vec.len (hashmap.List T) slots
   if i < i1