diff --git a/CHANGELOG.md b/CHANGELOG.md
index 54670738d570f38ba1cec56fc93ec6f4d7d1e900..2725b0cc9c33121b99fb445edb7c81472478b8f9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,22 @@ lemma.
   intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
   not dispose of hypotheses to perform the rewrite.
 
+**LaTeX changes:**
+
+- Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
+  with the Coq names and to avoid clash with hyperref package.
+
+The following sed script helps adjust LaTeX documents to these changes:
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- *.tex <<EOF
+# Alloc & Ref
+s/\\Alloc\b/\\AllocN/g
+s/\\Ref\b/\\Alloc/g
+EOF
+```
+
+
 ## Iris 4.0.0 (2022-08-18)
 
 The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
index 388781886b61355aba24aeddbdd133140aa117c7..a51959a9afaab359c3c93490dc009db3106bb3f7 100644
--- a/tex/heaplang.sty
+++ b/tex/heaplang.sty
@@ -26,7 +26,6 @@
 \def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac}
 \def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
 \def\Else{\spac\langkw{else} \spac}
-\def\Ref{\operatorname{\langkw{ref}}}
 \def\Rec#1#2={\langkw{rec}\spac\operatorname{#1}#2 \mathrel{=} }
 \def\Skip{\langkw{skip}}
 \def\Assert{\operatorname{\langkw{assert}}}
@@ -53,12 +52,14 @@
 \def\MatchS#1with#2=>#3end{
   \langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
 
-\newcommand\Alloc{\operatorname{\langkw{Alloc}}}
+\newcommand\AllocN{\operatorname{\langkw{AllocN}}}
+\newcommand\Alloc{\operatorname{\langkw{ref}}} % syntax rendering consistent with Coq
 \newcommand\Free{\operatorname{\langkw{Free}}}
 \newcommand\CAS{\operatorname{\langkw{CAS}}}
 \newcommand\CmpXchg{\operatorname{\langkw{CmpXchg}}}
 \newcommand\Xchg{\operatorname{\langkw{Xchg}}}
 \newcommand\FAA{\operatorname{\langkw{FAA}}}
+
 \newcommand\deref{\mathop{!}}
 \let\gets\leftarrow
 
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 32645b86631a12e905fd9b7493209bbcd73810fb..61e5ffcc6888f33d36c2d851437b58329fd6a149 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -39,7 +39,7 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
   \InrE(\expr) \mid
   \Match \expr with \Inl => \expr_1 | \Inr => \expr_2 end \mid
   {}\\ &
-  \Alloc(\expr_1,\expr_2) \mid
+  \AllocN(\expr_1,\expr_2) \mid
   \Free(\expr) \mid
   \deref \expr \mid
   \expr_1 \gets \expr_2 \mid
@@ -66,7 +66,7 @@ We will leave away the disambiguating subscript when it is clear from the contex
 All of this lets us define $\ofval$ as simply applying the value injection (the very first syntactic form of $\Expr$), which makes a lot of things in Coq much simpler.
 $\toval$ is defined recursively in the obvious way.
 
-\langkw{Alloc} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
+\langkw{AllocN} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
 This lets one allocate arrays.
 $\Ptradd$ implements pointer arithmetic (the left operand must be a pointer, the right operand an integer), which is used to access array elements.
 
@@ -103,8 +103,8 @@ The HeapLang operational semantics is defined via the use of \emph{evaluation co
   \Inr(\lctx) \mid
   \Match \lctx with \Inl => \expr_1 | \Inr => \expr_2 end \mid
   {}\\ &
-  \Alloc(\expr, \lctx) \mid
-  \Alloc(\lctx, \val) \mid
+  \AllocN(\expr, \lctx) \mid
+  \AllocN(\lctx, \val) \mid
   \Free(\lctx) \mid
   \deref \lctx \mid
   \expr \gets \lctx \mid
@@ -198,7 +198,7 @@ The $\HLOp$ subscript indicates that this is the HeapLang operator, not the math
 \newcommand\alignheader{\kern-30ex}
 \begin{align*}
 &\alignheader\textbf{Heap reductions} \\
-(\Alloc(z, \val), \state) \hstep[\nil]{}&
+(\AllocN(z, \val), \state) \hstep[\nil]{}&
   (\loc, \mapinsert {[\loc,\loc+z)} \val {\state:\stateHeap}, \nil)
   &&\text{if $z>0$ and \(\All i<z. \state.\stateHeap(\loc+i) = \bot\)} \\
 (\Free(\loc), \state) \hstep[\nil]{}&
@@ -231,7 +231,7 @@ The $\HLOp$ subscript indicates that this is the HeapLang operator, not the math
 \end{mathpar}
 \caption{HeapLang impure reduction rules. \\ \small
 Here, $\state:\stateHeap$ denotes $\sigma$ with the $\stateHeap$ field updated as indicated.
-$[\loc,\loc+z)$ in the $\Alloc$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
+$[\loc,\loc+z)$ in the $\AllocN$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
 \label{fig:heaplang-reduction-impure}
 \end{figure}
 
@@ -282,7 +282,7 @@ We recover many of the common language operations as syntactic sugar.
   \expr_1 \mathop{||} \expr_2 \eqdef{}& \If \expr_1 then \True \Else \expr_2 \\
   \Match \expr with \Inl(\lvar) => \expr_1 | \Inr(\lvarB) => \expr_2 end \eqdef {}&
     \Match \expr with \Inl => \Lam\lvar. \expr_1 | \Inr => \Lam\lvarB. \expr_2 end \\
-  \Ref(\expr) \eqdef{}& \Alloc(1,\expr) \\
+  \Alloc(\expr) \eqdef{}& \AllocN(1,\expr) \\
   \CAS(\expr_1, \expr_2, \expr_3) \eqdef{}& \Snd(\CmpXchg(\expr_1, \expr_2, \expr_3)) \\
   \Resolve \expr_1 to \expr_2 \eqdef{}& \ResolveWith \Skip at \expr_1 to \expr_2
 \end{align*}
diff --git a/tex/test.tex b/tex/test.tex
index e5fb6fce57b00febf94d56778dd63bb5101f0840..cdcbf73fa6e633e79fd2436ab013410d33d26645 100644
--- a/tex/test.tex
+++ b/tex/test.tex
@@ -58,7 +58,7 @@ Here we put a bunch of uses of the macros in \texttt{iris.sty} that we can visua
 \newcommand\OScheck{\textlang{check}}
 
     \begin{proofoutline*}
-       \CODE{\Let \lvar = \Ref(\Inl(0)) in } \\
+       \CODE{\Let \lvar = \Alloc(\Inl(0)) in } \\
        \RES{\lvar \mapsto \Inl(0) * \ownGhost\gname{\ospending(1)}}[\top] \quad\COMMENT{(\textsc{hoare-alloc}, \textsc{ghost-alloc})} \\
        \RES{\lvar \mapsto \Inl(0) * \ownGhost\gname{\ospending(1/2)} * \ownGhost\gname{\ospending(1/2)}}[\top] \quad\COMMENT{(\textsc{ghost-op})} \\
        \RES{\knowInv\namesp{I} * \ownGhost\gname{\ospending(1/2)}}[\top] \quad\COMMENT{(\textsc{inv-alloc1})} \\