diff --git a/spec/changelog.tex b/spec/changelog.tex
index 69bbc741f427a2a81abb5a8ecdbead12c4defd55..c088145b55fe924d08c4778c408fc0a60885f449 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -4,6 +4,11 @@ List of rules:
 \begin{itemize}
     \item Improve description of $\proofRule{sko\_ex}$.
 \end{itemize}
+\noindent
+Corrections:
+\begin{itemize}
+    \item Grammar: the \texttt{choice} binder can only bind one variable.
+\end{itemize}
 
 \noindent
 Clarifications:
@@ -14,6 +19,7 @@ Clarifications:
     \item Fix linear arithmetic example in introduction.
 \end{itemize}
 
+
 \subsection*{0.1 --- \DTMdisplaydate{2021}{07}{10}{-1}}
 
 This is the first public release of this document.  It coincides with
diff --git a/spec/doc.tex b/spec/doc.tex
index bc950bfdb8b13169b00d4b9d8352f7281f59659c..b1673e3f5402d58d4a0867a4c065f07011d4c7f9 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1033,28 +1033,27 @@ production for the $\grT{choice}$ binder.
       \grNT{proof\_command} &\grRule& \grT{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
                             &\grOr  & \grT{(step}\; \grNT{symbol}\; \grNT{clause}
                                       \; \grT{:rule}\; \grNT{symbol}\\
-                            &       & \quad\grNT{step\_annotation}\; \grT{)}\\
+                            &       & \quad\grNT{step\_annotation}^{?}\; \grT{)}\\
                             & \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\; \grT{)}\\
                             & \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\;
                                       \grT{:args}\; \grNT{proof\_args}\; \grT{)}\\
                             & \grOr & \grT{(define-fun}\; \grNT{function\_def}\; \grT{)}\\
       \grNT{clause}         &\grRule& \grT{(cl}\; \grNT{proof\_term}^{*}\; \grT{)}\\
-      \grNT{step\_annotation} &\grRule&
-                                      \grT{:premises (}\; \grNT{symbol}^{+}\; \grT{)}\;\\
-                            & \grOr & \grT{:args}\; \grNT{proof_args}\\
-                            & \grOr & \grT{:premises (}\; \grNT{symbol}^{+}\; \grT{)}\;
-                                      \grT{:args}\; \grNT{proof_args}\\
+
+      \grNT{step\_annotation} &\grRule& \grNT{premises\_annotation}^{?}\;\grNT{args\_annotation}\\
+
+      \grNT{premises\_annotation}  &\grRule& \grT{:premises (}\; \grNT{symbol}^{+}\grT{)}\\
+      \grNT{args\_annotation}      &\grRule& \grT{:args}\; \grNT{proof_args}\\
+
       \grNT{proof\_args}    &\grRule& \grT{(}\; \grNT{proof\_arg}^{+}\; \grT{)}\\
       \grNT{proof\_arg}     &\grRule& \grNT{symbol} \grOr
                                       \grT{(}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
       \grNT{proof\_term}    &\grRule& \grNT{term}\text{ extended with }\\
-                            &       & \grT{(choice (}\; \grNT{sorted\_var}^{+}\;\grT{)}\; \grNT{proof\_term}\; \grT{)}
+                            &       & \grT{(choice (}\; \grNT{sorted\_var}\;\grT{)}\; \grNT{proof\_term}\; \grT{)}
     \end{array}\]
   }\par}
 \caption{The proof grammar}\label{fig:grammar}
 \end{figure}
-% PF TODO: factorize <arg_annotation> and <premise_annotation>
-% PF TODO: introduce ^? to denote optional non-terminal
 
 Input problems in the SMT-LIB standard contain a list of \emph{commands}
 that modify the internal state of the solver. In agreement