diff --git a/ProgramDerivation_template.v b/ProgramDerivation_template.v
index 566ea1b..f7e368f 100644
--- a/ProgramDerivation_template.v
+++ b/ProgramDerivation_template.v
@@ -2,6 +2,8 @@ Require Import Frap.
 Require Import Program Setoids.Setoid Classes.RelationClasses Classes.Morphisms Morphisms_Prop.
 Require Import Eqdep.
 
+Set Warnings "-cannot-define-projection".
+
 Ltac inv_pair :=
   match goal with
   | [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; invert H
@@ -185,7 +187,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop)
     -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
                        (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
 
-Hint Constructors RefineMethods.
+Hint Constructors RefineMethods : core.
 
 Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
   ArRel : AdtState adt1 -> AdtState adt2 -> Prop;
@@ -212,7 +214,7 @@ Definition split_counter := ADT {
   and method "value"[[self, _]] = ret (self, fst self + snd self)
 }.
 
-Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic.
+Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core.
 
 Theorem split_counter_ok : adt_refine counter split_counter.
 Proof.
@@ -230,7 +232,7 @@ Proof.
   subst; eauto.
 Qed.  
 
-Hint Immediate RefineMethods_refl.
+Hint Immediate RefineMethods_refl : core.
 
 Theorem refine_refl : forall names (adt1 : adt names),
     adt_refine adt1 adt1.
@@ -259,7 +261,7 @@ Proof.
   first_order.
 Qed.
 
-Hint Resolve RefineMethods_trans.
+Hint Resolve RefineMethods_trans : core.
 
 Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
     adt_refine adt1 adt2
@@ -322,7 +324,7 @@ Proof.
   simplify; subst; eauto.
 Qed.
 
-Hint Resolve ReplaceMethod_ok.
+Hint Resolve ReplaceMethod_ok : core.
 
 Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))
                                names (ms1 ms2 : methods state names) constr,
@@ -367,7 +369,7 @@ Proof.
   eauto.
 Qed.
 
-Hint Resolve RepChangeMethods_ok.
+Hint Resolve RepChangeMethods_ok : core.
 
 Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
                             names (ms1 : methods state1 names) (ms2 : methods state2 names)
@@ -424,7 +426,7 @@ Inductive CachingMethods {state} (name : string) (func : state -> nat)
     CachingMethods name func ms1 ms2
     -> CachingMethods name func
        (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, func s)) |} ms1)
-       (MethodsCons {| MethodName := name; MethodBody := (fun s arg => ret (s, snd s)) |} ms2)
+       (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, snd s)) |} ms2)
 | CmDefault : forall name' names oldbody (ms1 : methods state names) (ms2 : methods _ names),
     name' <> name
     -> CachingMethods name func ms1 ms2
@@ -458,7 +460,7 @@ Proof.
   eauto.
 Qed.
 
-Hint Resolve CachingMethods_ok.
+Hint Resolve CachingMethods_ok : core.
 
 Theorem refine_cache : forall state name (func : state -> nat)
                             names (ms1 : methods state names) (ms2 : methods (state * nat) names)