diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 6d495e3..650d944 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -19,8 +19,8 @@ Set Asymmetric Patterns.
 Notation heap := (fmap nat nat).
 Notation locks := (set nat).
 
-Hint Extern 1 (_ <= _) => linear_arithmetic.
-Hint Extern 1 (@eq nat _ _) => linear_arithmetic.
+Hint Extern 1 (_ <= _) => linear_arithmetic : core.
+Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
 
 Ltac simp := repeat (simplify; subst; propositional;
                      try match goal with
@@ -206,7 +206,7 @@ Module Import S <: SEP.
     t.
   Qed.
 
-  Hint Resolve split_empty_bwd'.
+  Hint Resolve split_empty_bwd' : core.
 
   Theorem extra_lift : forall (P : Prop) p,
     P
@@ -488,7 +488,7 @@ Proof.
   apply try_me_first_easy.
 Qed.
 
-Hint Resolve try_ptsto_first.
+Hint Resolve try_ptsto_first : core.
 
 
 (** ** The nonzero shared counter *)
@@ -829,7 +829,7 @@ Qed.
  * book PDF for a sketch of the important technical devices and lemmas in this
  * proof. *)
 
-Hint Resolve himp_refl.
+Hint Resolve himp_refl : core.
 
 Lemma invert_Return : forall linvs {result : Set} (r : result) P Q,
   hoare_triple linvs P (Return r) Q
@@ -844,7 +844,7 @@ Proof.
   rewrite IHhoare_triple; eauto.
 Qed.
 
-Hint Constructors hoare_triple.
+Hint Constructors hoare_triple : core.
 
 Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
   hoare_triple linvs P (Bind c1 c2) Q
diff --git a/frap_book.tex b/frap_book.tex
index b8ada22..989abaf 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4745,7 +4745,7 @@ Here's the object language we adopt, which should be old hat by now, just mixing
 
 $$\begin{array}{rrcl}
   \textrm{Commands} & c &::=& \mt{Fail} \mid \mt{Return} \; v \mid x \leftarrow c; c \mid \mt{Loop} \; i \; f \\
-  &&& \mid \mt{Read} \; a \mid \mt{Write} \; a \; v \mid \mt{Lock} \; a \mid \mt{Unlock} \; a \mid c || c
+  &&& \mid \mt{Read} \; a \mid \mt{Write} \; a \; v \mid \mt{Alloc} \; n \mid \mt{Free} \; a \; n \mid \mt{Lock} \; a \mid \mt{Unlock} \; a \mid c || c
 \end{array}$$
 
 $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{
@@ -4762,6 +4762,12 @@ $$\infer{\smallstep{(h, l, \mt{Read} \; a)}{(h, l, \mt{Return} \; v)}}{
   \msel{h}{a} = v
 }$$
 
+$$\infer{\smallstep{(h, \mt{Alloc} \; n)}{(\mupd{h}{a}{0^n}, \mt{Return} \; a)}}{
+  \dom{h} \cap [a, a+n) = \emptyset
+}
+\quad \infer{\smallstep{(h, \mt{Free} \; a \; n)}{(h - [a, a+n), \mt{Return} \; ())}}{
+}$$
+
 $$\infer{\smallstep{(h, l, \mt{Lock} \; a)}{(h, l \cup \{a\}, \mt{Return} \; ())}}{
   a \notin l
 }