Fix some more references

1 files changed, 4 insertions, 3 deletions

diff --git a/chapters/hls.tex b/chapters/hls.tex
index 6a6809f..f39afd3 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -1191,10 +1191,10 @@ matching state.
 %
   \NC \text{\sc Load}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm
       r}[\mathit{r.u_{en}}]\qquad \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 0}{((\Gamma_{\rm r},
-    \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), r) \downarrow_{\text{ram}} (\Delta_{\rm
+    \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), r) \downarrow_{\text{ram}} \left(\Delta_{\rm
       r}\left[\startmatrix[n=1]
 \NC\mathit{r.en} \mapsto \mathit{r.u_{en}},\NR
-\NC\mathit{r.d_{out}} \mapsto (\Gamma_{\rm a}[\mathit{r.mem}\NR\stopmatrix\right])[ \mathit{r.addr}]], \Delta_{\rm a}) }\NR
+\NC\mathit{r.d_{out}} \mapsto (\Gamma_{\rm a}[\mathit{r.mem}])[ \mathit{r.addr}]\NR\stopmatrix\right], \Delta_{\rm a}\right) }\NR
 %
   \NC \text{\sc Store}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm r}[\mathit{r.u_{en}}]\qquad
     \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 1}{((\Gamma_{\rm r}, \Gamma_{\rm a}), (\Delta_{\rm r},
@@ -1317,7 +1317,8 @@ $B_1$ and $B_2$ must be the same.
 
 \subsection[coq-mechanisation]{Coq Mechanisation}
 
-\startplacetable[reference=tab:proof-statistics]
+\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of
+    code in the proof and implementation of Vericert.}]
   \starttabulate[|l|r|r|r|r|r|]
     \FL
     \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR