Add some tiny changes and upgrades to the proof section

1 files changed, 1 insertions, 1 deletions

diff --git a/verilog.tex b/verilog.tex
index 1e0b9ff..11087b0 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -92,7 +92,7 @@ The \compcert{} computation model defines a set of states through which executio
 \compcert{} executions pass through three main states:
 \begin{description}
   \item[\texttt{State} $\mathit{sf}$ $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame $\mathit{sf}$, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$.
-  \item[\texttt{Callstate} $\mathit{sf}$ ${r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.
+  \item[\texttt{Callstate} $\mathit{sf}$ $m$ $\vec{r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.
   \item[\texttt{Returnstate} $\mathit{sf}$ $v$] The state that is reached when a function returns back to the caller, with stack frame $\mathit{sf}$ and return value $v$.
 \end{description}