--- a/src/InductiveTypes.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/InductiveTypes.v	Sun Jul 31 14:48:22 2022 -0400
@@ -479,7 +479,7 @@
 (* end thide *)
 End list.
 
-Arguments Nil [T].
+Arguments Nil {T}.
 
 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)