Some tweaks/fixes

compcertoe/compcertoe.tex

@@ -4762,7 +4762,8 @@ \section{Evaluation and Applications} \label{sec:app} %{{{
 
 \subsection{Mechanization in the Coq Proof Assistant} \label{sec:application:impl} %{{{
 
-Our code uses a library called $\kw{coqrel}$ \cite{coqrel}
+Our code uses a library called $\kw{coqrel}$%
+\footnote{\url{http://certikos.github.io/coqrel/}}
 for relational reasoning
 and the relevant parts interface with CompCertO as well.
 In addition,
@@ -4776,8 +4777,8 @@ \subsection{Mechanization in the Coq Proof Assistant} \label{sec:application:imp
 With these dependencies,
 the definitions and theorems 
 given in \S\ref{sec:overview}--\ref{sec:scomp}
-can be mechanized in $2,198$ lines of Coq definitions and
-$3,252$ lines of proofs, as counted by $\kw{coqwc}$.
+can be mechanized in $2{,}198$ lines of Coq definitions and
+$3{,}252$ lines of proofs, as counted by $\kw{coqwc}$.
 The mechanization
 is straightforward and closely follows the definitions we have given.