1 files changed, 24 insertions, 0 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex
index dcdf2b2..1a5374c 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -1317,6 +1317,29 @@ $B_1$ and $B_2$ must be the same.
 
 \subsection[coq-mechanisation]{Coq Mechanisation}
 
+\startnotmode[nolmtx]
+\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
+    \ML
+    \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR
+    \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR
+    \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR
+    \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR
+    \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR
+    \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR
+    \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR
+    \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR
+    \LL
+    \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR
+    \BL
+  \stoptabulate
+\stopplacetable
+\stopnotmode
+
+\startmode[nolmtx]
 \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|]
@@ -1336,6 +1359,7 @@ $B_1$ and $B_2$ must be the same.
     \HL
   \stoptabulate
 \stopplacetable
+\stopmode
 
 The lines of code for the implementation and proof of can be found in
 \in{Table}[tab:proof-statistics]. Overall, it took about 1.5 person-years to build -- about three