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) :=