--- a/src/DataStruct.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/DataStruct.v	Sun Jan 20 15:28:23 2019 -0500
@@ -243,10 +243,10 @@
 
 (* begin thide *)
 Arguments HNil [A B].
-Arguments HCons [A B x ls].
+Arguments HCons [A B x ls] _ _.
 
 Arguments HFirst [A elm ls].
-Arguments HNext [A elm x 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. *)
@@ -481,7 +481,7 @@
 
 End fhlist.
 
-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.
 
-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.
 
-Arguments rifoldr [A B] f i [n].
+Arguments rifoldr [A B] f i [n] _.
 
 Fixpoint sum (t : tree nat) : nat :=
   match t with
@@ -708,7 +708,7 @@
     end.
 End cond.
 
-Arguments cond [A] default [n].
+Arguments cond [A] default [n] _ _.
 (* end thide *)
 
 (** Now the expression interpreter is straightforward to write. *)
@@ -797,7 +797,7 @@
     end.
 End cfoldCond.
 
-Arguments cfoldCond [t] default [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. *)