--- a/src/DataStruct.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/DataStruct.v	Sun Jul 31 14:48:22 2022 -0400
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Arguments Nil [A].
-Arguments First [n].
+Arguments Nil {A}.
+Arguments First {n}.
 
 (** A few examples show how to make use of these definitions. *)
 
@@ -242,10 +242,10 @@
 End hlist.
 
 (* begin thide *)
-Arguments HNil [A B].
+Arguments HNil {A B}.
 Arguments HCons [A B x ls] _ _.
 
-Arguments HFirst [A elm ls].
+Arguments HFirst {A elm ls}.
 Arguments HNext [A elm x ls] _.
 (* end thide *)
 
@@ -302,7 +302,7 @@
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
 
-Arguments Const [ts].
+Arguments Const {ts}.
 
 (** We write a simple recursive function to translate [type]s into [Set]s. *)