summaryrefslogtreecommitdiff
path: root/tests/coq/misc/Paper.v
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Paper.v4
1 files changed, 2 insertions, 2 deletions
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 :=