diff --git a/AbstractInterpret.v b/AbstractInterpret.v
index 141b1ca..7ade533 100644
--- a/AbstractInterpret.v
+++ b/AbstractInterpret.v
@@ -56,7 +56,7 @@ Record absint_sound (a : absint) : Prop := {
                                  -> a.(Represents) n (a.(Join) x y)
 }.
 
-Hint Resolve TopSound ConstSound AddSound SubtractSound MultiplySound
+Global Hint Resolve TopSound ConstSound AddSound SubtractSound MultiplySound
      AddMonotone SubtractMonotone MultiplyMonotone
      JoinSoundLeft JoinSoundRight : core.
 
@@ -103,7 +103,7 @@ Proof.
   cases (s $? x); equality.
 Qed.
 
-Hint Resolve subsumed_refl : core.
+Global Hint Resolve subsumed_refl : core.
 
 Lemma subsumed_use : forall a (s s' : astate a) x n t0 t,
   s $? x = Some t0
@@ -131,7 +131,7 @@ Proof.
   equality.
 Qed.
 
-Hint Resolve subsumed_use subsumed_use_empty : core.
+Global Hint Resolve subsumed_use subsumed_use_empty : core.
 
 Lemma subsumed_trans : forall a (s1 s2 s3 : astate a),
   subsumed s1 s2
@@ -156,7 +156,7 @@ Proof.
   invert H0; eauto.
 Qed.
 
-Hint Resolve subsumed_merge_left : core.
+Global Hint Resolve subsumed_merge_left : core.
 
 Lemma subsumed_add : forall a, absint_sound a
   -> forall (s1 s2 : astate a) x v1 v2,
@@ -170,7 +170,7 @@ Proof.
   specialize (H0 x0); eauto.
 Qed.
 
-Hint Resolve subsumed_add : core.
+Global Hint Resolve subsumed_add : core.
 
 
 (** * Flow-sensitive analysis *)
@@ -190,7 +190,7 @@ Proof.
   invert H1; eauto.
 Qed.
 
-Hint Resolve compatible_add : core.
+Global Hint Resolve compatible_add : core.
 
 (* A similar result follows about soundness of expression interpretation. *)
 Theorem absint_interp_ok : forall a, absint_sound a
@@ -208,7 +208,7 @@ Proof.
   assumption.
 Qed.
 
-Hint Resolve absint_interp_ok : core.
+Global Hint Resolve absint_interp_ok : core.
 
 Definition astates (a : absint) := fmap cmd (astate a).
 
@@ -281,7 +281,7 @@ Inductive abs_step a : astate a * cmd -> astate a * cmd -> Prop :=
   -> ss $? c' = Some s'
   -> abs_step (s, c) (s', c').
 
-Hint Constructors abs_step : core.
+Global Hint Constructors abs_step : core.
 
 Definition absint_trsys a (c : cmd) := {|
   Initial := {($0, c)};
@@ -293,7 +293,7 @@ Inductive Rabsint a : valuation * cmd -> astate a * cmd -> Prop :=
   compatible s v
   -> Rabsint (v, c) (s, c).
 
-Hint Constructors abs_step Rabsint : core.
+Global Hint Constructors abs_step Rabsint : core.
 
 Theorem absint_simulates : forall a v c,
   absint_sound a
@@ -351,7 +351,7 @@ Proof.
   unfold subsumeds; simplify; eauto.
 Qed.
 
-Hint Resolve subsumeds_refl : core.
+Global Hint Resolve subsumeds_refl : core.
 
 Lemma subsumeds_add : forall a (ss1 ss2 : astates a) c s1 s2,
   subsumeds ss1 ss2
@@ -363,7 +363,7 @@ Proof.
   invert H1; eauto.
 Qed.
 
-Hint Resolve subsumeds_add : core.
+Global Hint Resolve subsumeds_add : core.
 
 Lemma subsumeds_empty : forall a (ss : astates a),
   subsumeds $0 ss.
@@ -459,7 +459,7 @@ Proof.
   cases (s $? x); eauto.
 Qed.
 
-Hint Resolve absint_interp_monotone : core.
+Global Hint Resolve absint_interp_monotone : core.
 
 Lemma absint_step_monotone : forall a, absint_sound a
     -> forall (s : astate a) c wrap ss,
diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 3cdd1ec..4b16787 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -474,7 +474,7 @@ Ltac use H := (eapply use_lemma; [ eapply H | cancel; auto ])
 Ltac heq := intros; apply himp_heq; split.
 
 (* Fancy theorem to help us rewrite within preconditions and postconditions *)
-Instance hoare_triple_morphism : forall linvs A,
+Local Instance hoare_triple_morphism : forall linvs A,
   Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple linvs A).
 Proof.
   Transparent himp.
diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v
index 9eb44e8..09ae9a8 100644
--- a/ConcurrentSeparationLogic_template.v
+++ b/ConcurrentSeparationLogic_template.v
@@ -455,7 +455,7 @@ Ltac use H := (eapply use_lemma; [ eapply H | cancel ])
 Ltac heq := intros; apply himp_heq; split.
 
 (* Fancy theorem to help us rewrite within preconditions and postconditions *)
-Instance hoare_triple_morphism : forall linvs A,
+Local Instance hoare_triple_morphism : forall linvs A,
   Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple linvs A).
 Proof.
   Transparent himp.
diff --git a/Connecting.v b/Connecting.v
index de98097..83753c7 100644
--- a/Connecting.v
+++ b/Connecting.v
@@ -769,7 +769,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
     cases s; simp; eauto.
   Qed.
 
-  Instance hoare_triple_morphism : forall A,
+  Local Instance hoare_triple_morphism : forall A,
     Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A).
   Proof.
     Transparent himp.
@@ -874,8 +874,8 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
                            end; cancel.
   Qed.
 
-  Hint Rewrite <- rev_alt.
-  Hint Rewrite rev_involutive.
+  Local Hint Rewrite <- rev_alt.
+  Local Hint Rewrite rev_involutive.
 
   Opaque linkedList.
 
diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v
index c0459ef..7d61779 100644
--- a/DeepAndShallowEmbeddings.v
+++ b/DeepAndShallowEmbeddings.v
@@ -19,7 +19,7 @@ Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
 
 Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
 
-Hint Rewrite max_l max_r using linear_arithmetic : core.
+Local Hint Rewrite max_l max_r using linear_arithmetic : core.
 
 Ltac simp := repeat (simplify; subst; propositional;
                      try match goal with
@@ -1214,7 +1214,7 @@ Module DeeperWithFail.
     reflexivity.
   Qed.
 
-  Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core.
+  Local Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core.
 
   (* Here's the soundness theorem for [heapfold], relying on a hypothesis of
    * soundness for [combine]. *)
diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v
index c0cfe9d..de1a6e6 100644
--- a/DeepAndShallowEmbeddings_template.v
+++ b/DeepAndShallowEmbeddings_template.v
@@ -14,7 +14,7 @@ Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
 
 Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
 
-Hint Rewrite max_l max_r using linear_arithmetic : core.
+Local Hint Rewrite max_l max_r using linear_arithmetic : core.
 
 Ltac simp := repeat (simplify; subst; propositional;
                      try match goal with
@@ -1044,7 +1044,7 @@ Module DeeperWithFail.
     reflexivity.
   Qed.
 
-  Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core.
+  Local Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core.
 
   Theorem heapfold_ok : forall {A : Set} (init : A) combine
                                (ls : list nat) (f : A -> nat -> A),
diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v
index 3811ec1..80816c7 100644
--- a/DependentInductiveTypes.v
+++ b/DependentInductiveTypes.v
@@ -1091,7 +1091,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite substring_all substring_none.
+Local Hint Rewrite substring_all substring_none.
 
 Lemma substring_split : forall s m,
   substring 0 m s ++ substring m (length s - m) s = s.
@@ -1115,7 +1115,7 @@ Proof.
   rewrite IHs1; auto.
 Qed.
 
-Hint Rewrite <- minus_n_O.
+Local Hint Rewrite <- minus_n_O.
 
 Lemma substring_app_snd : forall s2 s1 n,
   length s1 = n
@@ -1124,7 +1124,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! *)
 
@@ -1227,7 +1227,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite app_empty_end.
+Local Hint Rewrite app_empty_end.
 
 Lemma substring_self : forall s n,
   n <= 0
@@ -1243,8 +1243,8 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite substring_self substring_empty using linear_arithmetic.
-Hint Rewrite substring_split.
+Local Hint Rewrite substring_self substring_empty using linear_arithmetic.
+Local Hint Rewrite substring_split.
 
 Lemma substring_split' : forall s n m,
   substring n m s ++ substring (n + m) (length s - (n + m)) s
@@ -1308,7 +1308,7 @@ Proof.
   simplify; cases m; simplify; eauto using substring_suffix_emp'.
 Qed.
 
-Hint Rewrite substring_stack substring_stack' substring_suffix using linear_arithmetic.
+Local Hint Rewrite substring_stack substring_stack' substring_suffix using linear_arithmetic.
 
 Lemma minus_minus : forall n m1 m2,
   m1 + m2 <= n
@@ -1322,7 +1322,7 @@ Proof.
   linear_arithmetic.
 Qed.
 
-Hint Rewrite minus_minus plus_n_Sm' using linear_arithmetic.
+Local Hint Rewrite minus_minus plus_n_Sm' using linear_arithmetic.
 
 (* BOREDOM VANQUISHED! *)
 
diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v
index 6303133..c213935 100644
--- a/DependentInductiveTypes_template.v
+++ b/DependentInductiveTypes_template.v
@@ -507,7 +507,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite substring_all substring_none.
+Local Hint Rewrite substring_all substring_none.
 
 Lemma substring_split : forall s m,
   substring 0 m s ++ substring m (length s - m) s = s.
@@ -531,7 +531,7 @@ Proof.
   rewrite IHs1; auto.
 Qed.
 
-Hint Rewrite <- minus_n_O.
+Local Hint Rewrite <- minus_n_O.
 
 Lemma substring_app_snd : 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! *)
 
@@ -609,7 +609,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite app_empty_end.
+Local Hint Rewrite app_empty_end.
 
 Lemma substring_self : forall s n,
   n <= 0
@@ -625,8 +625,8 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Rewrite substring_self substring_empty using linear_arithmetic.
-Hint Rewrite substring_split.
+Local Hint Rewrite substring_self substring_empty using linear_arithmetic.
+Local Hint Rewrite substring_split.
 
 Lemma substring_split' : forall s n m,
   substring n m s ++ substring (n + m) (length s - (n + m)) s
@@ -690,7 +690,7 @@ Proof.
   simplify; cases m; simplify; eauto using substring_suffix_emp'.
 Qed.
 
-Hint Rewrite substring_stack substring_stack' substring_suffix using linear_arithmetic.
+Local Hint Rewrite substring_stack substring_stack' substring_suffix using linear_arithmetic.
 
 Lemma minus_minus : forall n m1 m2,
   m1 + m2 <= n
@@ -704,7 +704,7 @@ Proof.
   linear_arithmetic.
 Qed.
 
-Hint Rewrite minus_minus plus_n_Sm' using linear_arithmetic.
+Local Hint Rewrite minus_minus plus_n_Sm' using linear_arithmetic.
 
 (* BOREDOM VANQUISHED! *)
 
diff --git a/FirstClassFunctions.v b/FirstClassFunctions.v
index a33c2b5..dd58c21 100644
--- a/FirstClassFunctions.v
+++ b/FirstClassFunctions.v
@@ -354,7 +354,7 @@ Proof.
   trivial.
 Qed.
 
-Hint Rewrite dnot_dnot.
+Global Hint Rewrite dnot_dnot.
 
 Lemma map_identity : forall A (f : A -> A) (ls : list A),
     (forall x, x = f x)
@@ -363,7 +363,7 @@ Proof.
   induct ls; simplify; equality.
 Qed.
 
-Hint Rewrite map_identity map_map using assumption.
+Global Hint Rewrite map_identity map_map using assumption.
 
 Lemma map_same : forall A B (f1 f2 : A -> B) ls,
     (forall x, f1 x = f2 x)
@@ -399,9 +399,9 @@ Proof.
   apply filter_same; assumption.
 Qed.
 
-Hint Resolve List_map_same List_filter_same : core.
+Global Hint Resolve List_map_same List_filter_same : core.
 
-Hint Extern 5 (_ = match _ with Bool _ => _ | _ => _ end) =>
+Global Hint Extern 5 (_ = match _ with Bool _ => _ | _ => _ end) =>
     match goal with
     | [ H : forall x : dyn, _ |- _ ] => rewrite <- H
     end : core.
@@ -493,7 +493,7 @@ Proof.
   induct d; simplify; linear_arithmetic.
 Qed.
 
-Hint Immediate dsize_positive : core.
+Global Hint Immediate dsize_positive : core.
 
 Lemma sum_map_monotone : forall A (f1 f2 : A -> nat) ds,
     (forall x, f1 x <= f2 x)
diff --git a/HoareLogic.v b/HoareLogic.v
index 41863a2..de5a668 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -316,7 +316,7 @@ Proof.
   simplify; subst; auto.
 Qed.
 
-Hint Rewrite <- minus_n_O.
+Local Hint Rewrite <- minus_n_O.
 
 Lemma fact_rec : forall n,
   n > 0
@@ -325,7 +325,7 @@ Proof.
   simplify; cases n; simplify; linear_arithmetic.
 Qed.
 
-Hint Rewrite fact_base fact_rec using linear_arithmetic.
+Local Hint Rewrite fact_base fact_rec using linear_arithmetic.
 
 (* Note the careful choice of loop invariant below.  It may look familiar from
  * earlier chapters' proofs! *)
diff --git a/Imp.v b/Imp.v
index aec61ee..96762c1 100644
--- a/Imp.v
+++ b/Imp.v
@@ -90,7 +90,7 @@ Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
   interp e v = 0
   -> step (v, While e body) (v, Skip).
 
-Hint Constructors trc step eval : core.
+Global Hint Constructors trc step eval : core.
 
 Lemma step_star_Seq : forall v c1 c2 v' c1',
   step^* (v, c1) (v', c1')
@@ -100,7 +100,7 @@ Proof.
   cases y; eauto.
 Qed.
 
-Hint Resolve step_star_Seq : core.
+Global Hint Resolve step_star_Seq : core.
 
 Theorem big_small : forall v c v', eval v c v'
   -> step^* (v, c) (v', Skip).
@@ -118,7 +118,7 @@ Proof.
          end; eauto.
 Qed.
 
-Hint Resolve small_big'' : core.
+Global Hint Resolve small_big'' : core.
 
 Lemma small_big' : forall v c v' c', step^* (v, c) (v', c')
                                      -> forall v'', eval v' c' v''
@@ -128,7 +128,7 @@ Proof.
   cases y; eauto.
 Qed.
 
-Hint Resolve small_big' : core.
+Global Hint Resolve small_big' : core.
 
 Theorem small_big : forall v c v', step^* (v, c) (v', Skip)
                                    -> eval v c v'.
@@ -176,7 +176,7 @@ Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
   -> plug C c' c2
   -> cstep (v, c1) (v', c2).
 
-Hint Constructors plug step0 cstep : core.
+Global Hint Constructors plug step0 cstep : core.
 
 Theorem step_cstep : forall v c v' c',
   step (v, c) (v', c')
@@ -187,7 +187,7 @@ Proof.
                    end; eauto.
 Qed.
 
-Hint Resolve step_cstep : core.
+Global Hint Resolve step_cstep : core.
 
 Lemma step0_step : forall v c v' c',
   step0 (v, c) (v', c')
@@ -196,7 +196,7 @@ Proof.
   invert 1; eauto.
 Qed.
 
-Hint Resolve step0_step : core.
+Global Hint Resolve step0_step : core.
 
 Lemma cstep_step' : forall C c0 c,
   plug C c0 c
@@ -209,7 +209,7 @@ Proof.
                              end; eauto.
 Qed.
 
-Hint Resolve cstep_step' : core.
+Global Hint Resolve cstep_step' : core.
 
 Theorem cstep_step : forall v c v' c',
   cstep (v, c) (v', c')
diff --git a/Map.v b/Map.v
index 24844f7..14c1267 100644
--- a/Map.v
+++ b/Map.v
@@ -133,17 +133,17 @@ Module Type S.
     lookup (restrict P m) k = Some v
     -> P k.
 
-  Hint Extern 1 => match goal with
+  Global Hint Extern 1 => match goal with
                      | [ H : lookup (empty _ _) _ = Some _ |- _ ] =>
                        rewrite lookup_empty in H; discriminate
                    end : core.
 
-  Hint Resolve includes_lookup includes_add empty_includes : core.
+  Global Hint Resolve includes_lookup includes_add empty_includes : core.
 
-  Hint Rewrite lookup_empty lookup_add_eq lookup_add_ne lookup_remove_eq lookup_remove_ne
+  Global Hint Rewrite lookup_empty lookup_add_eq lookup_add_ne lookup_remove_eq lookup_remove_ne
        lookup_merge lookup_restrict_true lookup_restrict_false using congruence.
 
-  Hint Rewrite dom_empty dom_add.
+  Global Hint Rewrite dom_empty dom_add.
 
   Ltac maps_equal :=
     apply fmap_ext; intros;
@@ -152,17 +152,17 @@ Module Type S.
           | [ |- context[lookup (add _ ?k _) ?k' ] ] => destruct (classic (k = k')); subst
         end).
 
-  Hint Extern 3 (_ = _) => maps_equal : core.
+  Global Hint Extern 3 (_ = _) => maps_equal : core.
 
   Axiom lookup_split : forall A B (m : fmap A B) k v k' v',
     (m $+ (k, v)) $? k' = Some v'
     -> (k' <> k /\ m $? k' = Some v') \/ (k' = k /\ v' = v).
 
-  Hint Rewrite merge_empty1 merge_empty2 using solve [ eauto 1 ].
-  Hint Rewrite merge_empty1_alt merge_empty2_alt using congruence.
+  Global Hint Rewrite merge_empty1 merge_empty2 using solve [ eauto 1 ].
+  Global Hint Rewrite merge_empty1_alt merge_empty2_alt using congruence.
 
-  Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
-  Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
+  Global Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
+  Global Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
 
   Axiom includes_intro : forall K V (m1 m2 : fmap K V),
       (forall k v, m1 $? k = Some v -> m2 $? k = Some v)
@@ -267,9 +267,9 @@ Module Type S.
       -> disjoint h3 h2.
   End splitting.
 
-  Hint Immediate disjoint_comm split_comm : core.
-  Hint Immediate split_empty_bwd disjoint_hemp disjoint_hemp' split_assoc1 split_assoc2 : core.
-  Hint Immediate disjoint_assoc1 disjoint_assoc2 split_join split_disjoint disjoint_assoc3 : core.
+  Global Hint Immediate disjoint_comm split_comm : core.
+  Global Hint Immediate split_empty_bwd disjoint_hemp disjoint_hemp' split_assoc1 split_assoc2 : core.
+  Global Hint Immediate disjoint_assoc1 disjoint_assoc2 split_join split_disjoint disjoint_assoc3 : core.
 End S.
 
 Module M : S.
diff --git a/SepCancel.v b/SepCancel.v
index 71b46ff..03d1f60 100644
--- a/SepCancel.v
+++ b/SepCancel.v
@@ -82,7 +82,7 @@ Module Make(Import S : SEP).
     transitivity proved by heq_trans
     as heq_rel.
 
-  Instance himp_heq_mor : Proper (heq ==> heq ==> iff) himp.
+  Global Instance himp_heq_mor : Proper (heq ==> heq ==> iff) himp.
   Proof.
     hnf; intros; hnf; intros.
     apply himp_heq in H; apply himp_heq in H0.
@@ -104,7 +104,7 @@ Module Make(Import S : SEP).
     auto using star_cancel.
   Qed.
 
-  Instance exis_iff_morphism (A : Type) :
+  Global Instance exis_iff_morphism (A : Type) :
     Proper (pointwise_relation A heq ==> heq) (@exis A).
   Proof.
     hnf; intros; apply himp_heq; intuition.
@@ -120,7 +120,7 @@ Module Make(Import S : SEP).
     apply himp_heq in H0; intuition eauto.
   Qed.
 
-  Instance exis_imp_morphism (A : Type) :
+  Global Instance exis_imp_morphism (A : Type) :
     Proper (pointwise_relation A himp ==> himp) (@exis A).
   Proof.
     hnf; intros.
diff --git a/SeparationLogic.v b/SeparationLogic.v
index 3c436fa..e059a86 100644
--- a/SeparationLogic.v
+++ b/SeparationLogic.v
@@ -181,7 +181,7 @@ Module Import S <: SEP.
     t.
   Qed.
 
-  Hint Resolve split_empty_bwd' : core.
+  Local Hint Resolve split_empty_bwd' : core.
 
   Theorem extra_lift : forall (P : Prop) p,
     P
@@ -1161,8 +1161,8 @@ Proof.
                          end; cancel.
 Qed.
 
-Hint Rewrite <- rev_alt.
-Hint Rewrite rev_involutive.
+Local Hint Rewrite <- rev_alt.
+Local Hint Rewrite rev_involutive.
 
 (* Let's hide the definition of [linkedList], so that we *only* reason about it
  * via the two lemmas we just proved. *)
@@ -1302,8 +1302,8 @@ Qed.
 Opaque linkedList linkedListSegment.
 
 (* A few algebraic properties of list operations: *)
-Hint Rewrite <- app_assoc.
-Hint Rewrite app_length app_nil_r.
+Local Hint Rewrite <- app_assoc.
+Local Hint Rewrite app_length app_nil_r.
 
 (* We tie a few of them together into this lemma. *)
 Lemma move_along : forall A (ls : list A) x2 x1 x0 x,
diff --git a/SeparationLogic_template.v b/SeparationLogic_template.v
index dce0b58..5006301 100644
--- a/SeparationLogic_template.v
+++ b/SeparationLogic_template.v
@@ -165,7 +165,7 @@ Module Import S <: SEP.
     t.
   Qed.
 
-  Hint Resolve split_empty_bwd' : core.
+  Global Hint Resolve split_empty_bwd' : core.
 
   Theorem extra_lift : forall (P : Prop) p,
     P
@@ -398,7 +398,7 @@ Qed.
 
 
 (* Fancy theorem to help us rewrite within preconditions and postconditions *)
-Instance hoare_triple_morphism : forall A,
+Local Instance hoare_triple_morphism : forall A,
   Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A).
 Proof.
   Transparent himp.
@@ -542,8 +542,8 @@ Proof.
                          end; cancel.
 Qed.
 
-Hint Rewrite <- rev_alt.
-Hint Rewrite rev_involutive.
+Local Hint Rewrite <- rev_alt.
+Local Hint Rewrite rev_involutive.
 
 (* Let's hide the definition of [linkedList], so that we *only* reason about it
  * via the two lemmas we just proved. *)
@@ -590,8 +590,8 @@ Admitted.
 (* ** Computing the length of a linked list *)
 
 (* A few algebraic properties of list operations: *)
-Hint Rewrite <- app_assoc.
-Hint Rewrite app_length app_nil_r.
+Local Hint Rewrite <- app_assoc.
+Local Hint Rewrite app_length app_nil_r.
 
 (* We tie a few of them together into this lemma. *)
 Lemma move_along : forall A (ls : list A) x2 x1 x0 x,
diff --git a/SubsetTypes.v b/SubsetTypes.v
index a9044b7..b1df979 100644
--- a/SubsetTypes.v
+++ b/SubsetTypes.v
@@ -536,7 +536,7 @@ Notation "e1 ;; e2" := (if e1 then e2 else ??)
  * [hasType] proof obligation, and [eauto] makes short work of them when we add
  * [hasType]'s constructors as hints. *)
 
-Local Hint Constructors hasType.
+Local Hint Constructors hasType : core.
 
 Definition typeCheck : forall e : exp, {{t | hasType e t}}.
   refine (fix F (e : exp) : {{t | hasType e t}} :=
@@ -589,7 +589,7 @@ Qed.
 (* Now we can define the type-checker.  Its type expresses that it only fails on
  * untypable expressions. *)
 
-Local Hint Resolve hasType_det.
+Local Hint Resolve hasType_det : core.
 (* The lemma [hasType_det] will also be useful for proving proof obligations
  * with contradictory contexts. *)