diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v
index d5a3935..3811ec1 100644
--- a/DependentInductiveTypes.v
+++ b/DependentInductiveTypes.v
@@ -141,13 +141,10 @@ Section ilist.
     | Cons _ h _ => h
     end.
 
-  (* Unlike in ML, we cannot use inexhaustive pattern matching, because there is
-   * no conception of a <<Match>> exception to be thrown.  In fact, recent
-   * versions of Coq _do_ allow this, by implicit translation to a [match] that
-   * considers all constructors; the error message above was generated by an
-   * older Coq version.  It is educational to discover for ourselves the
-   * encoding that the most recent Coq versions use.  We might try using an [in]
-   * clause somehow. *)
+  (* Actually, these days, Coq is smart enough to make that definition work!
+   * However, it will be educational to look at how Coq elaborates this code
+   * into its core language, where, unlike in ML, all pattern matching must be
+   * _exhaustive_.  We might try using an [in] clause somehow. *)
 
   Fail Fail Definition hd n (ls : ilist (S n)) : A :=
     match ls in (ilist (S n)) with
@@ -173,13 +170,22 @@ Section ilist.
   Check hd'.
 
   Definition hd n (ls : ilist (S n)) : A := hd' ls.
-End ilist.
 
-(* We annotate our main [match] with a type that is itself a [match].  We write
- * that the function [hd'] returns [unit] when the list is empty and returns the
- * carried type [A] in all other cases.  In the definition of [hd], we just call
- * [hd'].  Because the index of [ls] is known to be nonzero, the type checker
- * reduces the [match] in the type of [hd'] to [A]. *)
+  (* We annotate our main [match] with a type that is itself a [match].  We
+   * write that the function [hd'] returns [unit] when the list is empty and
+   * returns the carried type [A] in all other cases.  In the definition of [hd],
+   * we just call [hd'].  Because the index of [ls] is known to be nonzero, the
+   * type checker reduces the [match] in the type of [hd'] to [A]. *)
+  
+  (* In fact, when we "got lucky" earlier with Coq accepting simpler
+   * definitions, under the hood it was desugaring _almost_ to this one. *)
+  Definition easy_hd n (ls : ilist (S n)) : A :=
+    match ls with
+    | Cons _ h _ => h
+    end.
+
+  Print easy_hd.
+End ilist.
 
 
 (** * The One Rule of Dependent Pattern Matching in Coq *)
@@ -330,7 +336,7 @@ Fixpoint expDenote t (e : exp t) : typeDenote t :=
   match e with
     | NConst n => n
     | Plus e1 e2 => expDenote e1 + expDenote e2
-    | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
+    | Eq e1 e2 => if expDenote e1 ==n expDenote e2 then true else false
 
     | BConst b => b
     | And e1 e2 => expDenote e1 && expDenote e2
@@ -345,10 +351,10 @@ Fixpoint expDenote t (e : exp t) : typeDenote t :=
  * less complicated than what we would write in ML or Haskell 98, since we do
  * not need to worry about pushing final values in and out of an algebraic
  * datatype.  The only unusual thing is the use of an expression of the form
- * [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has
+ * [if E then true else false] in the [Eq] case.  Remember that [==n] has
  * a rich dependent type, rather than a simple Boolean type.  Coq's native [if]
  * is overloaded to work on a test of any two-constructor type, so we can use
- * [if] to build a simple Boolean from the [sumbool] that [eq_nat_dec] returns.
+ * [if] to build a simple Boolean from the [sumbool] that [==n] returns.
  *
  * We can implement our old favorite, a constant-folding function, and prove it
  * correct.  It will be useful to write a function [pairOut] that checks if an
@@ -387,10 +393,7 @@ Definition pairOut t (e : exp t) :=
 
 (* With [pairOut] available, we can write [cfold] in a straightforward way.
  * There are really no surprises beyond that Coq verifies that this code has
- * such an expressive type, given the small annotation burden.  In some places,
- * we see that Coq's [match] annotation inference is too smart for its own
- * good, and we have to turn that inference off with explicit [return]
- * clauses. *)
+ * such an expressive type, given the small annotation burden. *)
 
 Fixpoint cfold t (e : exp t) : exp t :=
   match e with
@@ -398,14 +401,14 @@ Fixpoint cfold t (e : exp t) : exp t :=
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Nat with
+      match e1', e2' with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Bool with
+      match e1', e2' with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
@@ -414,7 +417,7 @@ Fixpoint cfold t (e : exp t) : exp t :=
     | And e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Bool with
+      match e1', e2' with
         | BConst b1, BConst b2 => BConst (b1 && b2)
         | _, _ => And e1' e2'
       end
@@ -488,9 +491,6 @@ Proof.
             end; simplify); try equality.
 Qed.
 
-(* With this example, we get a first taste of how to build automated proofs that
- * adapt automatically to changes in function definitions. *)
-
 
 (** * Interlude: The Convoy Pattern *)
 
@@ -676,7 +676,7 @@ Section present.
 End present.
 
 (* Insertion relies on two balancing operations.  It will be useful to give types
- * to these operations using a relative of the subset types from last chapter.
+ * to these operations using a relative of the subset types from SubsetTypes.
  * While subset types let us pair a value with a proof about that value, here we
  * want to pair a value with another non-proof dependently typed value.  The
  * [sigT] type fills this role. *)
@@ -1071,7 +1071,7 @@ Ltac substring :=
              destruct N; simplify
          end; try linear_arithmetic; eauto; try equality.
 
-Hint Resolve le_n_S : core.
+Local Hint Resolve le_n_S : core.
 
 Lemma substring_le : forall s n m,
   length (substring n m s) <= m.
@@ -1105,7 +1105,7 @@ Proof.
   induct s1; substring.
 Qed.
 
-Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
+Local Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
 
 Lemma substring_app_fst : forall s2 s1 n,
   length s1 = n
@@ -1151,7 +1151,7 @@ End sumbool_and.
 
 Infix "&&" := sumbool_and (at level 40, left associativity).
 
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
 
 Section split.
   Variables P1 P2 : string -> Prop.
@@ -1253,7 +1253,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
+Local Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
 
 Lemma substring_stack : forall s n2 m1 m2,
   m1 <= m2
@@ -1507,7 +1507,7 @@ Proof.
   equality.
 Qed.
 
-Hint Resolve app_cong : core.
+Local Hint Resolve app_cong : core.
 
 (* With these helper functions completed, the implementation of our [matches]
  * function is refreshingly straightforward. *)
diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v
index 5ed2346..8c41e9b 100644
--- a/DependentInductiveTypes_template.v
+++ b/DependentInductiveTypes_template.v
@@ -91,14 +91,14 @@ Fixpoint cfold t (e : exp t) : exp t :=
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Nat with
+      match e1', e2' with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Bool with
+      match e1', e2' with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
@@ -107,7 +107,7 @@ Fixpoint cfold t (e : exp t) : exp t :=
     | And e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return exp Bool with
+      match e1', e2' with
         | BConst b1, BConst b2 => BConst (b1 && b2)
         | _, _ => And e1' e2'
       end
@@ -487,7 +487,7 @@ Ltac substring :=
              destruct N; simplify
          end; try linear_arithmetic; eauto; try equality.
 
-Hint Resolve le_n_S : core.
+Local Hint Resolve le_n_S : core.
 
 Lemma substring_le : forall s n m,
   length (substring n m s) <= m.
@@ -521,7 +521,7 @@ Proof.
   induct s1; substring.
 Qed.
 
-Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
+Local Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
 
 Lemma substring_app_fst : forall s2 s1 n,
   length s1 = n
@@ -540,7 +540,7 @@ Proof.
   induct s1; simplify; subst; simplify; auto.
 Qed.
 
-Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
+Local Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
 
 (* BOREDOM'S END! *)
 
@@ -563,7 +563,7 @@ End sumbool_and.
 
 Infix "&&" := sumbool_and (at level 40, left associativity).
 
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
 
 Section split.
   Variables P1 P2 : string -> Prop.
@@ -863,7 +863,7 @@ Proof.
   equality.
 Qed.
 
-Hint Resolve app_cong : core.
+Local Hint Resolve app_cong : core.
 
 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
   refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
diff --git a/HoareLogic.v b/HoareLogic.v
index 1ca0273..46e6f37 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -61,7 +61,7 @@ Fixpoint eval (e : exp) (h : heap) (v : valuation) : nat :=
   end.
 
 (* Meaning of Boolean expressions *)
-Fixpoint beval (b : bexp) (h : heap) (v : valuation) : bool :=
+Definition beval (b : bexp) (h : heap) (v : valuation) : bool :=
   match b with
   | Equal e1 e2 => if eval e1 h v ==n eval e2 h v then true else false
   | Less e1 e2 => if eval e2 h v <=? eval e1 h v then false else true
@@ -385,10 +385,10 @@ Proof.
   ht.
 Qed.
 
-Hint Resolve leq_f : core.
-Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
-Hint Extern 1 (_ < _) => linear_arithmetic : core.
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Resolve leq_f : core.
+Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ < _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
 (* We also register [linear_arithmetic] as a step to try during proof search. *)
 
 (* These invariants are fairly hairy, but probably the best way to understand
@@ -472,7 +472,7 @@ Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
   a h v
   -> step (h, v, Assert a) (h, v, Skip).
 
-Hint Constructors step : core.
+Local Hint Constructors step : core.
 
 Definition trsys_of (st : heap * valuation * cmd) := {|
   Initial := {st};
diff --git a/HoareLogic_template.v b/HoareLogic_template.v
index a196e23..d64d1b9 100644
--- a/HoareLogic_template.v
+++ b/HoareLogic_template.v
@@ -264,10 +264,10 @@ Proof.
   ht.
 Qed.
 
-Hint Resolve leq_f : core.
-Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
-Hint Extern 1 (_ < _) => linear_arithmetic : core.
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Resolve leq_f : core.
+Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ < _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
 (* We also register [linear_arithmetic] as a step to try during proof search. *)
 
 Theorem selectionSort_ok :
@@ -324,7 +324,7 @@ Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
   a h v
   -> step (h, v, Assert a) (h, v, Skip).
 
-Hint Constructors step : core.
+Local Hint Constructors step : core.
 
 Definition trsys_of (st : heap * valuation * cmd) := {|
   Initial := {st};
diff --git a/frap_book.tex b/frap_book.tex
index a38d393..f0e0e9b 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -3903,7 +3903,6 @@ We call any such fact a \emph{Hoare triple}\index{Hoare triple}, and the overall
 
 \encoding
 A first rule for $\skipe$ is easy: anything that was true before is also true after.
-
 $$\infer{\hoare{P}{\skipe}{P}}{}$$
 
 A rule for assignment is slightly more involved: to state what we know is true after, we recall that there existed a prestate satisfying the precondition, which then evolved into the poststate in the expected way.
@@ -4045,7 +4044,7 @@ $$\infer{\smallstep{(h, v, \assert{a})}{(h, v, \skipe)}}{
 Even an infinite-looping program must satisfy its $\mathsf{assert}$ commands, every time it passes one of them.
 For that reason, it's interesting to consider how to show that a command never gets stuck on a false assertion.
 We work up to that result with a few intermediate ones.
-First, we define \emph{stuck} much the same way as in the last two chapters: a state $(h, v, c)$ is stuck if $c$ is not $\skipe$, but there is also nowhere to step to from this state.
+First, we define \emph{stuck} much the same way as in the last three chapters: a state $(h, v, c)$ is stuck if $c$ is not $\skipe$, but there is also nowhere to step to from this state.
 An example of a stuck state would be one beginning with an $\mathsf{assert}$ of an assertion that does not hold on $h$ and $v$.
 In fact, we can prove that any other state is unstuck, though we won't bother here.