Commit e78029cb authored by Piotr Trojanek's avatar Piotr Trojanek Committed by Guillaume Melquiond

Fix documentation typos.

parent cfbca94a
...@@ -18,7 +18,7 @@ phases: ...@@ -18,7 +18,7 @@ phases:
An example of such an interaction is given in the tutorial An example of such an interaction is given in the tutorial
section~\ref{sec:gui}. section~\ref{sec:gui}.
Some proof assistants offer more than one possible editor, e.g. a Some proof assistants offer more than one possible editor, \eg a
choice between the use of a dedicated editor and the use of the Emacs choice between the use of a dedicated editor and the use of the Emacs
editor and the ProofGeneral mode. Selection of the preferred mode can editor and the ProofGeneral mode. Selection of the preferred mode can
be made in \texttt{why3ide} preferences, under the ``Editors'' tab. be made in \texttt{why3ide} preferences, under the ``Editors'' tab.
......
...@@ -448,7 +448,7 @@ end ...@@ -448,7 +448,7 @@ end
Alternatively, we can implement the search with a \texttt{while} loop. Alternatively, we can implement the search with a \texttt{while} loop.
To do this, we need to import references from the standard library, To do this, we need to import references from the standard library,
together with theory \texttt{list.HdTl} which defines function together with theory \texttt{list.HdTl} which defines functions
\texttt{hd} and \texttt{tl} over lists. \texttt{hd} and \texttt{tl} over lists.
\begin{whycode} \begin{whycode}
use import ref.Ref use import ref.Ref
......
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