Commit b6216b9e authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Fixed more typos in the appendix

parent 4df2f959
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
\lstinputlisting[language=diff]{tweetnacl.diff} \lstinputlisting[language=diff]{tweetnacl.diff}
As follow, we provide the explanations of the above changes to TweetNaCl's code. In the following, we provide the explanations of the above changes to TweetNaCl's code.
\begin{itemize} \begin{itemize}
\item lines 7-8: We tell VST that \TNaCle{long long} are \item lines 7-8: We tell VST that \TNaCle{long long} are
......
...@@ -2,10 +2,10 @@ ...@@ -2,10 +2,10 @@
\label{appendix:proof-folders} \label{appendix:proof-folders}
\subheading{Requirements.} \subheading{Requirements.}
Our proofs requires the use of \emph{Coq 8.8.2} for the proofs and Our proofs require the use of \emph{Coq 8.8.2} and
\emph{Opam 2.0} to manage the dependencies. We are aware that there exists more \emph{Opam 2.0} to manage the dependencies. We are aware that there exist more
recent versions of Coq; VST; CompCert etc. however to avoid dealing with backward recent versions of Coq; VST; CompCert etc. However, to avoid dealing with backward
breaking compatibility we decided to freeze our dependencies. compatibility issues, we decided to freeze our dependencies.
\subheading{Associated files.} \subheading{Associated files.}
The repository containing the proof is composed of two folders \textbf{\texttt{packages}} The repository containing the proof is composed of two folders \textbf{\texttt{packages}}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment