summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon Ho2023-11-09 16:24:07 +0100
committerSon Ho2023-11-09 16:24:07 +0100
commit49ffc966cfdbd71f8c83a3c72ab81e1bb101f420 (patch)
treea60e31612f0049a7b3d1c2e616b3f18c230f7f82 /tests/coq/misc
parent3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 (diff)
Regenerate the Coq test files
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Constants.v10
-rw-r--r--tests/coq/misc/Loops.v4
-rw-r--r--tests/coq/misc/NoNestedBorrows.v32
-rw-r--r--tests/coq/misc/Paper.v4
-rw-r--r--tests/coq/misc/PoloniusList.v4
5 files changed, 27 insertions, 27 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 7cb1a642..03653f69 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -35,9 +35,9 @@ Definition mk_pair0 (x : u32) (y : u32) : result (u32 * u32) :=
(** [constants::Pair] *)
Record Pair_t (T1 T2 : Type) := mkPair_t { pair_x : T1; pair_y : T2; }.
-Arguments mkPair_t {T1} {T2} _ _.
-Arguments pair_x {T1} {T2}.
-Arguments pair_y {T1} {T2}.
+Arguments mkPair_t { _ _ }.
+Arguments pair_x { _ _ }.
+Arguments pair_y { _ _ }.
(** [constants::mk_pair1]: forward function *)
Definition mk_pair1 (x : u32) (y : u32) : result (Pair_t u32 u32) :=
@@ -65,8 +65,8 @@ Definition p3_c : Pair_t u32 u32 := p3_body%global.
(** [constants::Wrap] *)
Record Wrap_t (T : Type) := mkWrap_t { wrap_value : T; }.
-Arguments mkWrap_t {T} _.
-Arguments wrap_value {T}.
+Arguments mkWrap_t { _ }.
+Arguments wrap_value { _ }.
(** [constants::Wrap::{0}::new]: forward function *)
Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) :=
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 180a1d68..1c0eab17 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -96,8 +96,8 @@ Inductive List_t (T : Type) :=
| List_Nil : List_t T
.
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [loops::list_mem]: loop 0: forward function *)
Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index e916ca4a..c7af496f 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -11,9 +11,9 @@ Module NoNestedBorrows.
(** [no_nested_borrows::Pair] *)
Record Pair_t (T1 T2 : Type) := mkPair_t { pair_x : T1; pair_y : T2; }.
-Arguments mkPair_t {T1} {T2} _ _.
-Arguments pair_x {T1} {T2}.
-Arguments pair_y {T1} {T2}.
+Arguments mkPair_t { _ _ }.
+Arguments pair_x { _ _ }.
+Arguments pair_y { _ _ }.
(** [no_nested_borrows::List] *)
Inductive List_t (T : Type) :=
@@ -21,13 +21,13 @@ Inductive List_t (T : Type) :=
| List_Nil : List_t T
.
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [no_nested_borrows::One] *)
Inductive One_t (T1 : Type) := | One_One : T1 -> One_t T1.
-Arguments One_One {T1} _.
+Arguments One_One { _ }.
(** [no_nested_borrows::EmptyEnum] *)
Inductive EmptyEnum_t := | EmptyEnum_Empty : EmptyEnum_t.
@@ -44,8 +44,8 @@ Inductive Sum_t (T1 T2 : Type) :=
| Sum_Right : T2 -> Sum_t T1 T2
.
-Arguments Sum_Left {T1} {T2} _.
-Arguments Sum_Right {T1} {T2} _.
+Arguments Sum_Left { _ _ }.
+Arguments Sum_Right { _ _ }.
(** [no_nested_borrows::neg_test]: forward function *)
Definition neg_test (x : i32) : result i32 :=
@@ -258,11 +258,11 @@ with NodeElem_t (T : Type) :=
| NodeElem_Nil : NodeElem_t T
.
-Arguments Tree_Leaf {T} _.
-Arguments Tree_Node {T} _ _ _.
+Arguments Tree_Leaf { _ }.
+Arguments Tree_Node { _ }.
-Arguments NodeElem_Cons {T} _ _.
-Arguments NodeElem_Nil {T}.
+Arguments NodeElem_Cons { _ }.
+Arguments NodeElem_Nil { _ }.
(** [no_nested_borrows::list_length]: forward function *)
Fixpoint list_length (T : Type) (l : List_t T) : result u32 :=
@@ -425,8 +425,8 @@ mkStructWithTuple_t {
}
.
-Arguments mkStructWithTuple_t {T1} {T2} _.
-Arguments structWithTuple_p {T1} {T2}.
+Arguments mkStructWithTuple_t { _ _ }.
+Arguments structWithTuple_p { _ _ }.
(** [no_nested_borrows::new_tuple1]: forward function *)
Definition new_tuple1 : result (StructWithTuple_t u32 u32) :=
@@ -450,8 +450,8 @@ mkStructWithPair_t {
}
.
-Arguments mkStructWithPair_t {T1} {T2} _.
-Arguments structWithPair_p {T1} {T2}.
+Arguments mkStructWithPair_t { _ _ }.
+Arguments structWithPair_p { _ _ }.
(** [no_nested_borrows::new_pair1]: forward function *)
Definition new_pair1 : result (StructWithPair_t u32 u32) :=
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index d397995b..d3852e6b 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -55,8 +55,8 @@ Inductive List_t (T : Type) :=
| List_Nil : List_t T
.
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [paper::list_nth_mut]: forward function *)
Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T :=
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index 4f804b55..4848444f 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -14,8 +14,8 @@ Inductive List_t (T : Type) :=
| List_Nil : List_t T
.
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [polonius_list::get_list_at_x]: forward function *)
Fixpoint get_list_at_x (ls : List_t u32) (x : u32) : result (List_t u32) :=