diff --git a/AbstractInterpret.v b/AbstractInterpret.v
index ea6033e..141b1ca 100644
--- a/AbstractInterpret.v
+++ b/AbstractInterpret.v
@@ -58,7 +58,7 @@ Record absint_sound (a : absint) : Prop := {
 
 Hint Resolve TopSound ConstSound AddSound SubtractSound MultiplySound
      AddMonotone SubtractMonotone MultiplyMonotone
-     JoinSoundLeft JoinSoundRight.
+     JoinSoundLeft JoinSoundRight : core.
 
 
 
@@ -103,7 +103,7 @@ Proof.
   cases (s $? x); equality.
 Qed.
 
-Hint Resolve subsumed_refl.
+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.
+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.
+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.
+Hint Resolve subsumed_add : core.
 
 
 (** * Flow-sensitive analysis *)
@@ -190,7 +190,7 @@ Proof.
   invert H1; eauto.
 Qed.
 
-Hint Resolve compatible_add.
+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.
+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.
+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.
+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.
+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.
+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.
+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/CompilerCorrectness_template.v b/CompilerCorrectness_template.v
index 99e93fe..e357280 100644
--- a/CompilerCorrectness_template.v
+++ b/CompilerCorrectness_template.v
@@ -26,6 +26,7 @@ Inductive cmd :=
 
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
+Declare Scope arith_scope.
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
@@ -100,7 +101,7 @@ Inductive generate : valuation * cmd -> list (option nat) -> Prop :=
   -> generate vc' ns
   -> generate vc (Some n :: ns).
 
-Hint Constructors plug step0 cstep generate.
+Hint Constructors plug step0 cstep generate : core.
 
 Definition traceInclusion (vc1 vc2 : valuation * cmd) :=
   forall ns, generate vc1 ns -> generate vc2 ns.
@@ -130,8 +131,8 @@ Example month_boundaries_in_days :=
     done
   done.
 
-Hint Extern 1 (interp _ _ = _) => simplify; equality.
-Hint Extern 1 (interp _ _ <> _) => simplify; equality.
+Hint Extern 1 (interp _ _ = _) => simplify; equality : core.
+Hint Extern 1 (interp _ _ <> _) => simplify; equality : core.
 
 Theorem first_few_values :
   generate ($0, month_boundaries_in_days) [Some 28; Some 56].
@@ -250,7 +251,7 @@ Proof.
   equality.
 Qed.
 
-Hint Resolve peel_cseq.
+Hint Resolve peel_cseq : core.
 
 Lemma plug_deterministic : forall v C c1 c2, plug C c1 c2
   -> forall l vc1, step0 (v, c1) l vc1
@@ -438,7 +439,7 @@ Proof.
   invert H4.
 Qed.
 
-Hint Resolve silent_generate_fwd silent_generate_bwd generate_Skip.
+Hint Resolve silent_generate_fwd silent_generate_bwd generate_Skip : core.
 
 Section simulation_skipping.
   Variable R : nat -> valuation * cmd -> valuation * cmd -> Prop.
@@ -526,7 +527,7 @@ Section simulation_skipping.
     clear; induct 1; eauto.
   Qed.
 
-  Hint Resolve step_to_termination.
+  Hint Resolve step_to_termination : core.
 
   Lemma R_Skip : forall n vc1 v,
       R n vc1 (v, Skip)
@@ -592,9 +593,9 @@ Section simulation_skipping.
   Qed.
 End simulation_skipping.
 
-Hint Extern 1 (_ < _) => linear_arithmetic.
-Hint Extern 1 (_ >= _) => linear_arithmetic.
-Hint Extern 1 (_ <> _) => linear_arithmetic.
+Hint Extern 1 (_ < _) => linear_arithmetic : core.
+Hint Extern 1 (_ >= _) => linear_arithmetic : core.
+Hint Extern 1 (_ <> _) => linear_arithmetic : core.
 
 Lemma cfold_ok : forall v c,
     (v, c) =| (v, cfold c).
@@ -835,7 +836,7 @@ Section simulation_multiple.
   (* We won't comment on the other proof details, though they could be
    * interesting reading. *)
 
-  Hint Constructors generateN.
+  Hint Constructors generateN : core.
 
   Lemma generateN_fwd : forall sc vc ns,
       generateN sc vc ns
@@ -844,7 +845,7 @@ Section simulation_multiple.
     induct 1; eauto.
   Qed.
 
-  Hint Resolve generateN_fwd.
+  Hint Resolve generateN_fwd : core.
 
   Lemma generateN_bwd : forall vc ns,
       generate vc ns
@@ -1061,7 +1062,7 @@ Proof.
   first_order.
 Qed.
 
-Hint Resolve agree_add agree_add_tempVar_fwd agree_add_tempVar_bwd agree_add_tempVar_bwd_prime agree_refl.
+Hint Resolve agree_add agree_add_tempVar_fwd agree_add_tempVar_bwd agree_add_tempVar_bwd_prime agree_refl : core.
 
 Lemma silent_csteps_front : forall c v1 v2 c1 c2,
     silent_cstep^* (v1, c1) (v2, c2)
@@ -1072,7 +1073,7 @@ Proof.
   eauto 6.
 Qed.
 
-Hint Resolve silent_csteps_front.
+Hint Resolve silent_csteps_front : core.
 
 Lemma tempVar_contra : forall n1 n2,
     tempVar n1 = tempVar n2
@@ -1083,7 +1084,7 @@ Proof.
   first_order.
 Qed.
 
-Hint Resolve tempVar_contra.
+Hint Resolve tempVar_contra : core.
 
 Lemma self_prime_contra : forall s,
     (s ++ "'")%string = s -> False.
@@ -1091,7 +1092,7 @@ Proof.
   induct s; simplify; equality.
 Qed.
 
-Hint Resolve self_prime_contra.
+Hint Resolve self_prime_contra : core.
 
 Opaque tempVar.
 
diff --git a/Imp.v b/Imp.v
index 494c92d..e349a8a 100644
--- a/Imp.v
+++ b/Imp.v
@@ -19,6 +19,7 @@ Inductive cmd :=
 
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
+Declare Scope arith_scope.
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
@@ -89,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.
+Hint Constructors trc step eval : core.
 
 Lemma step_star_Seq : forall v c1 c2 v' c1',
   step^* (v, c1) (v', c1')
@@ -99,7 +100,7 @@ Proof.
   cases y; eauto.
 Qed.
 
-Hint Resolve step_star_Seq.
+Hint Resolve step_star_Seq : core.
 
 Theorem big_small : forall v c v', eval v c v'
   -> step^* (v, c) (v', Skip).
@@ -117,7 +118,7 @@ Proof.
          end; eauto.
 Qed.
 
-Hint Resolve small_big''.
+Hint Resolve small_big'' : core.
 
 Lemma small_big' : forall v c v' c', step^* (v, c) (v', c')
                                      -> forall v'', eval v' c' v''
@@ -127,7 +128,7 @@ Proof.
   cases y; eauto.
 Qed.
 
-Hint Resolve small_big'.
+Hint Resolve small_big' : core.
 
 Theorem small_big : forall v c v', step^* (v, c) (v', Skip)
                                    -> eval v c v'.
@@ -175,7 +176,7 @@ Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
   -> plug C c' c2
   -> cstep (v, c1) (v', c2).
 
-Hint Constructors plug step0 cstep.
+Hint Constructors plug step0 cstep : core.
 
 Theorem step_cstep : forall v c v' c',
   step (v, c) (v', c')
@@ -186,7 +187,7 @@ Proof.
                    end; eauto.
 Qed.
 
-Hint Resolve step_cstep.
+Hint Resolve step_cstep : core.
 
 Lemma step0_step : forall v c v' c',
   step0 (v, c) (v', c')
@@ -195,7 +196,7 @@ Proof.
   invert 1; eauto.
 Qed.
 
-Hint Resolve step0_step.
+Hint Resolve step0_step : core.
 
 Lemma cstep_step' : forall C c0 c,
   plug C c0 c
@@ -208,7 +209,7 @@ Proof.
                              end; eauto.
 Qed.
 
-Hint Resolve cstep_step'.
+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 b097f56..6953e4d 100644
--- a/Map.v
+++ b/Map.v
@@ -136,9 +136,9 @@ Module Type S.
   Hint Extern 1 => match goal with
                      | [ H : lookup (empty _ _) _ = Some _ |- _ ] =>
                        rewrite lookup_empty in H; discriminate
-                   end.
+                   end : core.
 
-  Hint Resolve includes_lookup includes_add empty_includes.
+  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
        lookup_merge lookup_restrict_true lookup_restrict_false using congruence.
@@ -152,7 +152,7 @@ Module Type S.
           | [ |- context[lookup (add _ ?k _) ?k' ] ] => destruct (classic (k = k')); subst
         end).
 
-  Hint Extern 3 (_ = _) => maps_equal.
+  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'
@@ -267,9 +267,9 @@ Module Type S.
       -> disjoint h3 h2.
   End splitting.
 
-  Hint Immediate disjoint_comm split_comm.
-  Hint Immediate split_empty_bwd disjoint_hemp disjoint_hemp' split_assoc1 split_assoc2.
-  Hint Immediate disjoint_assoc1 disjoint_assoc2 split_join split_disjoint disjoint_assoc3.
+  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.
 End S.
 
 Module M : S.
@@ -593,7 +593,7 @@ Module M : S.
     Definition split (h h1 h2 : fmap K V) : Prop :=
       h = h1 $++ h2.
 
-    Hint Extern 2 (_ <> _) => congruence.
+    Hint Extern 2 (_ <> _) => congruence : core.
 
     Ltac splt := unfold disjoint, split, join, lookup in *; intros; subst;
                  try match goal with
@@ -661,7 +661,7 @@ Module M : S.
       splt.
     Qed.
 
-    Hint Immediate disjoint_comm split_comm.
+    Hint Immediate disjoint_comm split_comm : core.
 
     Lemma split_assoc1 : forall h h1 h' h2 h3,
       split h h1 h'
diff --git a/ModelCheck.v b/ModelCheck.v
index ef04754..cd77e36 100644
--- a/ModelCheck.v
+++ b/ModelCheck.v
@@ -143,7 +143,7 @@ Proof.
   eauto.
 Qed.
 
-Local Hint Constructors invariantViaSimulation.
+Local Hint Constructors invariantViaSimulation : core.
 
 Theorem invariant_simulates : forall state1 state2 (R : state1 -> state2 -> Prop)
   (sys1 : trsys state1) (sys2 : trsys state2) (inv2 : state2 -> Prop),
diff --git a/Relations.v b/Relations.v
index 7930bb3..3c7ea7b 100644
--- a/Relations.v
+++ b/Relations.v
@@ -12,7 +12,7 @@ Section trc.
     -> trc y z
     -> trc x z.
 
-  Hint Constructors trc.
+  Hint Constructors trc : core.
 
   Theorem trc_one : forall x y, R x y
     -> trc x y.
@@ -20,7 +20,7 @@ Section trc.
     eauto.
   Qed.
 
-  Hint Resolve trc_one.
+  Hint Resolve trc_one : core.
 
   Theorem trc_trans : forall x y, trc x y
     -> forall z, trc y z
@@ -29,7 +29,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trc_trans.
+  Hint Resolve trc_trans : core.
 
   Inductive trcEnd : A -> A -> Prop :=
   | TrcEndRefl : forall x, trcEnd x x
@@ -38,7 +38,7 @@ Section trc.
     -> R y z
     -> trcEnd x z.
 
-  Hint Constructors trcEnd.
+  Hint Constructors trcEnd : core.
 
   Lemma TrcFront' : forall x y z,
     R x y
@@ -48,7 +48,7 @@ Section trc.
     induction 2; eauto.
   Qed.
 
-  Hint Resolve TrcFront'.
+  Hint Resolve TrcFront' : core.
 
   Theorem trc_trcEnd : forall x y, trc x y
     -> trcEnd x y.
@@ -56,7 +56,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trc_trcEnd.
+  Hint Resolve trc_trcEnd : core.
 
   Lemma TrcBack' : forall x y z,
     trc x y
@@ -66,7 +66,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve TrcBack'.
+  Hint Resolve TrcBack' : core.
 
   Theorem trcEnd_trans : forall x y, trcEnd x y
     -> forall z, trcEnd y z
@@ -75,7 +75,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trcEnd_trans.
+  Hint Resolve trcEnd_trans : core.
   
   Theorem trcEnd_trc : forall x y, trcEnd x y
     -> trc x y.
@@ -83,7 +83,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trcEnd_trc.
+  Hint Resolve trcEnd_trc : core.
 
   Inductive trcLiteral : A -> A -> Prop :=
   | TrcLiteralRefl : forall x, trcLiteral x x
@@ -93,7 +93,7 @@ Section trc.
   | TrcInclude : forall x y, R x y
     -> trcLiteral x y.
 
-  Hint Constructors trcLiteral.
+  Hint Constructors trcLiteral : core.
 
   Theorem trc_trcLiteral : forall x y, trc x y
     -> trcLiteral x y.
@@ -107,7 +107,7 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trc_trcLiteral trcLiteral_trc.
+  Hint Resolve trc_trcLiteral trcLiteral_trc : core.
 
   Theorem trcEnd_trcLiteral : forall x y, trcEnd x y
     -> trcLiteral x y.
@@ -121,10 +121,10 @@ Section trc.
     induction 1; eauto.
   Qed.
 
-  Hint Resolve trcEnd_trcLiteral trcLiteral_trcEnd.
+  Hint Resolve trcEnd_trcLiteral trcLiteral_trcEnd : core.
 End trc.
 
 Notation "R ^*" := (trc R) (at level 0).
 Notation "*^ R" := (trcEnd R) (at level 0).
 
-Hint Constructors trc.
+Hint Constructors trc : core.
diff --git a/Sets.v b/Sets.v
index 49bf1f6..9be67e1 100644
--- a/Sets.v
+++ b/Sets.v
@@ -1,4 +1,4 @@
-Require Import Classical FunctionalExtensionality List.
+Require Import Bool Classical FunctionalExtensionality List.
 
 Set Implicit Arguments.
 
@@ -131,7 +131,7 @@ Section properties.
   Qed.
 End properties.
 
-Hint Resolve subseteq_refl subseteq_In.
+Hint Resolve subseteq_refl subseteq_In : core.
 
 (*Hint Rewrite union_constant.*)
 
@@ -506,8 +506,6 @@ Section setexpr.
     destruct (member a ns2); simpl in *; auto; congruence.
   Qed.
 
-  Require Import Bool.
-
   Theorem compare_sets : forall env e1 e2,
       let nf1 := normalize_setexpr e1 in
       let nf2 := normalize_setexpr e2 in