diff --git a/SeparationLogic.v b/SeparationLogic.v
index 7368414..6a9e3ba 100644
--- a/SeparationLogic.v
+++ b/SeparationLogic.v
@@ -12,8 +12,8 @@ Set Asymmetric Patterns.
 
 Definition heap := fmap nat nat.
 
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
-Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
 
 Ltac simp := repeat (simplify; subst; propositional;
                      try match goal with
@@ -376,7 +376,7 @@ Proof.
   unfold star, himp in *; simp; eauto 7.
 Qed.
 
-Hint Constructors hoare_triple : core.
+Local Hint Constructors hoare_triple : core.
 
 Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
   hoare_triple P (Bind c1 c2) Q
@@ -785,7 +785,7 @@ Proof.
   eauto using deallocate_None.
 Qed.
 
-Hint Constructors step : core.
+Local Hint Constructors step : core.
 
 Lemma progress : forall {result} (c : cmd result) P Q,
     hoare_triple P c Q
@@ -1313,7 +1313,7 @@ Proof.
   simp.
 Qed.
 
-Hint Resolve move_along : core.
+Local Hint Resolve move_along : core.
 
 Theorem length_ok : forall p ls,
   {{linkedList p ls}}
diff --git a/SeparationLogic_template.v b/SeparationLogic_template.v
index ba9916a..42df9ee 100644
--- a/SeparationLogic_template.v
+++ b/SeparationLogic_template.v
@@ -9,8 +9,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3
 Definition heap := fmap nat nat.
 Definition assertion := heap -> Prop.
 
-Hint Extern 1 (_ <= _) => linear_arithmetic : core.
-Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
+Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
 
 Ltac simp := repeat (simplify; subst; propositional;
                      try match goal with
@@ -601,7 +601,7 @@ Proof.
   simp.
 Qed.
 
-Hint Resolve move_along : core.
+Local Hint Resolve move_along : core.
 
 Theorem length_ok : forall p ls,
   {{linkedList p ls}}
@@ -637,7 +637,7 @@ Proof.
   unfold star, himp in *; simp; eauto 7.
 Qed.
 
-Hint Constructors hoare_triple : core.
+Local Hint Constructors hoare_triple : core.
 
 Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
   hoare_triple P (Bind c1 c2) Q
@@ -1033,7 +1033,7 @@ Proof.
   eauto using deallocate_None.
 Qed.
 
-Hint Constructors step : core.
+Local Hint Constructors step : core.
 
 Lemma progress : forall {result} (c : cmd result) P Q,
     hoare_triple P c Q
diff --git a/frap_book.tex b/frap_book.tex
index f0e0e9b..ed9e286 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4314,7 +4314,7 @@ In our Hoare-logic examples so far, we have intentionally tread lightly when it
 Generally, we have only worked with, for instance, a single array at a time.
 Reasoning about multi-array programs usually depends on the fact that the arrays don't overlap in memory at all.
 Things are even more complicated with linked data structures, like linked lists and trees, which we haven't even attempted up to now.
-However, by using \emph{separation logic}\index{separation logic}, a popular variant of Hoare logic, we will find it quite pleasant to prove programs that used linked structures, with no need for explicit reasoning about aliasing, assuming that we keep all of our data structures disjoint from each other through simple coding patterns.
+However, by using \emph{separation logic}\index{separation logic}, a popular variant of Hoare logic, we will find it quite pleasant to prove programs that use linked structures, with no need for explicit reasoning about aliasing, assuming that we keep all of our data structures disjoint from each other through simple coding patterns.
 
 
 \section{An Object Language with Dynamic Memory Allocation}