summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/arrays/_CoqProject2
-rw-r--r--tests/coq/betree/_CoqProject12
-rw-r--r--tests/coq/demo/_CoqProject2
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v2
-rw-r--r--tests/coq/hashmap/_CoqProject4
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v2
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject12
-rw-r--r--tests/coq/misc/_CoqProject24
-rw-r--r--tests/coq/traits/_CoqProject2
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst2
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst2
-rw-r--r--tests/lean/Hashmap/Funs.lean2
-rw-r--r--tests/lean/HashmapMain/Funs.lean2
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