Commit ecfa4816 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some documentation typos. Add an empty line at the end of...

Fix some documentation typos. Add an empty line at the end of replayer_macros.tex to work around a bug in hevea's lstlisting implementation.
parent 632a7d89
......@@ -12,4 +12,5 @@
\newcommand{\explanation}[1]{\cellcolor{yellow!13}\textsl{#1}}
\newcommand{\valid}[1]{\cellcolor{green!13}#1}
\newcommand{\unknown}{\cellcolor{red!20}?}
\ No newline at end of file
\newcommand{\unknown}{\cellcolor{red!20}?}
......@@ -226,7 +226,7 @@ TODO: raise, try with end
\subsubsection{Conditional expression, pattern matching}
if then else. Discuss standar WP versus fast WP
if then else. Discuss standard WP versus fast WP
\subsubsection{Loops}
......@@ -246,7 +246,7 @@ where \textsl{keyword} is either \texttt{assert}, \texttt{assume} or
\item \texttt{check} requires to prove that the proposition holds, but
does not make it visible in the remaining
\item \texttt{assume} assumes that the proposition holds and make it
visible in the context of the remiaing code, without requiring to
visible in the context of the remaining code, without requiring to
prove it. It acts like an axiom, but within a program.
\end{itemize}
The corresponding rules for computing WP are as follows:
......
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