--- a/src/DataStruct.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/DataStruct.v	Sun Jan 20 15:16:29 2019 -0500
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Implicit Arguments Nil [A].
-Implicit Arguments First [n].
+Arguments Nil [A].
+Arguments First [n].
 
 (** A few examples show how to make use of these definitions. *)
 
@@ -242,11 +242,11 @@
 End hlist.
 
 (* begin thide *)
-Implicit Arguments HNil [A B].
-Implicit Arguments HCons [A B x ls].
+Arguments HNil [A B].
+Arguments HCons [A B x ls].
 
-Implicit Arguments HFirst [A elm ls].
-Implicit Arguments HNext [A elm x ls].
+Arguments HFirst [A elm ls].
+Arguments HNext [A elm x ls].
 (* end thide *)
 
 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
@@ -302,7 +302,7 @@
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
 
-Implicit Arguments Const [ts].
+Arguments Const [ts].
 
 (** We write a simple recursive function to translate [type]s into [Set]s. *)
 
@@ -481,7 +481,7 @@
 
 End fhlist.
 
-Implicit Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls].
 
 (** How does one choose between the two data structure encoding strategies we have presented so far?  Before answering that question in this chapter's final section, we introduce one further approach. *)
 
@@ -592,7 +592,7 @@
 
 End tree.
 
-Implicit Arguments Node [A n].
+Arguments Node [A n].
 
 (** We can redefine [sum] and [inc] for our new [tree] type.  Again, it is useful to define a generic fold function first.  This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
 
@@ -608,7 +608,7 @@
     end.
 End rifoldr.
 
-Implicit Arguments rifoldr [A B n].
+Arguments rifoldr [A B] f i [n].
 
 Fixpoint sum (t : tree nat) : nat :=
   match t with
@@ -708,7 +708,7 @@
     end.
 End cond.
 
-Implicit Arguments cond [A n].
+Arguments cond [A] default [n].
 (* end thide *)
 
 (** Now the expression interpreter is straightforward to write. *)
@@ -797,7 +797,7 @@
     end.
 End cfoldCond.
 
-Implicit Arguments cfoldCond [t n].
+Arguments cfoldCond [t] default [n].
 (* end thide *)
 
 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)