diff --git a/spec/changelog.tex b/spec/changelog.tex
index 8fea177adeca471973c9433f8e11a3b083503faa..79db8373cd353a05d9a84988f8eaafeedcfcbf1d 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -5,6 +5,12 @@ Breaking changes:
   \item Allow arbitrary extra annotations in \texttt{assume} commands.
 \end{itemize}
 
+Clarifications:
+\begin{itemize}
+  \item Clarify that the \texttt{:args} annotation in \texttt{anchor} can be
+        omitted if the list is empty.
+\end{itemize}
+
 \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
 
 This release overhauls the entire document, but introduces only few
diff --git a/spec/doc.tex b/spec/doc.tex
index f68c66c324944b3760e8c28c18ca4be0ca277e54..49e333bc66ae4e01a5f2b475988badf282342f82 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -820,9 +820,14 @@ pushes precisely $c_1,\dots, c_n$ onto the context.
 Since contexts can only be manipulated by push and pop, context manipulations
 are nested.  The \inlineAlethe{anchor} commands push onto the context and the
 corresponding \inlineAlethe{step} commands pop from the context.
+%
 To indicate these changes to the context, every anchor is associated with a list
-of fixed variables and mappings.
-This list can be empty.
+of fixed variables and mappings.  The list is provided by the \inlineAlethe{:args}
+annotation.  If the list is empty, the \inlineAlethe{:args} annotation is
+omitted\footnote{The only rule that allows an empty list is the
+\proofRule{subproof} rule.  Since this rule corresponds to implication introduction,
+it does not interact with binders.}.
+%
 Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
 some mappings $x_1 \mapsto t_1, \dots,  x_n \mapsto t_n$,
 then the terms $t_i$ are normalized by applying