From e78029cbc34096ae790b53b50cdd38b1b726c365 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 29 Aug 2014 17:53:04 +0200 Subject: [PATCH] Fix documentation typos. --- doc/itp.tex | 2 +- doc/whyml.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/itp.tex b/doc/itp.tex index 658fc1b87..0755d6738 100644 --- a/doc/itp.tex +++ b/doc/itp.tex @@ -18,7 +18,7 @@ phases: An example of such an interaction is given in the tutorial 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 editor and the ProofGeneral mode. Selection of the preferred mode can be made in \texttt{why3ide} preferences, under the ``Editors'' tab. diff --git a/doc/whyml.tex b/doc/whyml.tex index 0cfb6260b..bd438c0a5 100644 --- a/doc/whyml.tex +++ b/doc/whyml.tex @@ -448,7 +448,7 @@ end Alternatively, we can implement the search with a \texttt{while} loop. 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. \begin{whycode} use import ref.Ref -- GitLab