diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v
index ec1b18d..309d2ed 100644
--- a/DeepAndShallowEmbeddings.v
+++ b/DeepAndShallowEmbeddings.v
@@ -14,8 +14,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.
 
 Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
 
@@ -494,6 +494,7 @@ Module Deep.
     eauto.
   Qed.
 End Deep.
+
 (* We use Coq's *extraction* feature to produce OCaml versions of our deeply
  * embedded programs.  Then we can run them using OCaml intepreters, which are
  * able to take advantage of the side effects built into OCaml, as a
@@ -839,6 +840,7 @@ End Deeper.
 
 Extraction "Deeper.ml" Deeper.index_of.
 
+
 (** * Adding the possibility of program failure *)
 
 (* Let's model another effect that can be implemented using native OCaml
@@ -1270,7 +1272,7 @@ Module DeeperWithFail.
     apply IHls; linear_arithmetic.
   Qed.
 
-  Hint Resolve le_max : core.
+  Local Hint Resolve le_max : core.
 
   (* Finally, a short proof of [array_max], appealing mostly to the generic
    * proof of [heapfold] *)
diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v
index dec4c7b..c0cfe9d 100644
--- a/DeepAndShallowEmbeddings_template.v
+++ b/DeepAndShallowEmbeddings_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.
 
 Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
 
@@ -1085,7 +1085,7 @@ Module DeeperWithFail.
     apply IHls; linear_arithmetic.
   Qed.
 
-  Hint Resolve le_max : core.
+  Local Hint Resolve le_max : core.
 
   Theorem array_max_ok : forall ls : list nat,
     {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}}