diff --git a/tex/heaplang.sty b/tex/heaplang.sty
index df6afc2ea7f40794a2d02362dc064ce4017361dc..50e739113bcafef1310c50c62cb40839b2301bdd 100644
--- a/tex/heaplang.sty
+++ b/tex/heaplang.sty
@@ -73,7 +73,7 @@
 \newcommand{\unfold}{\langkw{unfold}\spac}
 
 \newcommand{\HLOp}{\circledcirc}
-\newcommand{\Ptradd}{\mathop{+_{\langkw{l}}}}
+\newcommand{\Ptradd}{\mathop{+_{\langkw{L}}}}
 
 \newcommand{\TT}{()}
 \newcommand*\poison{\text{\Biohazard}}
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 0498d8222ab8ad6eaf07fd3bf419e9f59fec92a1..5bdf6e9c4e9108cd8f64b6a4c0e12369afde8cbe 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -66,6 +66,10 @@ 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.
+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.
+
 For our set of states and observations, we pick
 \begin{align*}
   \loc \ni \Loc \eqdef{}& \integer \\