diff --git a/.gitignore b/.gitignore
index 3090ba6..43c0b49 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,7 +12,7 @@
 Makefile.coq
 Makefile.coq.conf
 *.glob
-*.v.d
+*.d
 *.vo
 frap.tgz
 .coq-native
diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v
index 71ae07f..f9bdb90 100644
--- a/DeepAndShallowEmbeddings.v
+++ b/DeepAndShallowEmbeddings.v
@@ -886,7 +886,7 @@ Module DeeperWithFail.
   | Stepped (h : heap) (c : cmd result)
   | Failed.
 
-  Implicit Arguments Failed [result].
+  Arguments Failed {result}.
 
   Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
     match c with
diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v
index 5365fad..352d80c 100644
--- a/DeepAndShallowEmbeddings_template.v
+++ b/DeepAndShallowEmbeddings_template.v
@@ -731,7 +731,7 @@ Module DeeperWithFail.
   | Stepped (h : heap) (c : cmd result)
   | Failed.
 
-  Implicit Arguments Failed [result].
+  Arguments Failed {result}.
 
   Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
     match c with
diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v
index 9848008..3f513d6 100644
--- a/DependentInductiveTypes.v
+++ b/DependentInductiveTypes.v
@@ -1217,7 +1217,7 @@ Section split.
   Defined.
 End split.
 
-Implicit Arguments split [P1 P2].
+Arguments split {P1 P2}.
 
 (* And now, a few more boring lemmas.  Rejoin at "BOREDOM VANQUISHED", if you
  * like. *)
diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v
index 715ecda..464b53a 100644
--- a/DependentInductiveTypes_template.v
+++ b/DependentInductiveTypes_template.v
@@ -599,7 +599,7 @@ Section split.
   Defined.
 End split.
 
-Implicit Arguments split [P1 P2].
+Arguments split {P1 P2}.
 
 (* And now, a few more boring lemmas.  Rejoin at "BOREDOM VANQUISHED", if you
  * like. *)
diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index fdad783..acbaa88 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -1,5 +1,5 @@
 Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
-Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
+Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck.
 Require Import List.
 Export List ListNotations.
 Open Scope string_scope.
diff --git a/SharedMemory.v b/SharedMemory.v
index 2f77dbf..c460acc 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -776,25 +776,25 @@ Inductive boundRunningTime : cmd -> nat -> Prop :=
 
 (* Perhaps surprisingly, there exist commands that have no finite time bounds!
  * Mixed-embedding languages often have these counterintuitive properties. *)
+Fixpoint scribbly (n : nat) : cmd :=
+  match n with
+  | O => Return 0
+  | S n' => _ <- Write n' 0; scribbly n'
+  end.
+
+Lemma scribbly_time : forall n m,
+    boundRunningTime (scribbly n) m
+    -> m >= n.
+Proof.
+  induct n; invert 1; auto.
+  invert H2.
+  specialize (H4 n0).
+  apply IHn in H4.
+  linear_arithmetic.
+Qed.
+
 Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n.
 Proof.
-  Fixpoint scribbly (n : nat) : cmd :=
-    match n with
-    | O => Return 0
-    | S n' => _ <- Write n' 0; scribbly n'
-    end.
-
-  Lemma scribbly_time : forall n m,
-      boundRunningTime (scribbly n) m
-      -> m >= n.
-  Proof.
-    induct n; invert 1; auto.
-    invert H2.
-    specialize (H4 n0).
-    apply IHn in H4.
-    linear_arithmetic.
-  Qed.
-
   exists (n <- Read 0; scribbly n); propositional.
   invert H.
   specialize (H4 (S n2)).