--- a/src/MoreDep.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/MoreDep.v	Sun Jan 20 15:16:29 2019 -0500
@@ -647,7 +647,7 @@
 
   (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *)
 
-  Implicit Arguments makeRbtree [c n].
+  Arguments makeRbtree [c n].
 
   (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
 
@@ -917,7 +917,7 @@
   Defined.
 End split.
 
-Implicit Arguments split [P1 P2].
+Arguments split [P1 P2].
 
 (* begin hide *)
 Lemma app_empty_end : forall s, s ++ "" = s.