Commit 84f5160b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some documentation typos.

parent 53c37b87
......@@ -4,14 +4,14 @@
This chapter details the usage of each of the command-line tools
provided by the \why environment. These are as follows:
\begin{description}
\item[\texttt{why3config}] tool for managing the user's configuration,
\item[\texttt{why3config}] manages the user's configuration,
including the detection of installed provers.
\item[\texttt{why3}] reads \why\ and \whyml input files and calls
provers, on the command-line.
\item[\texttt{why3ide}] graphical interface to display goals, run
provers and transformations on them.
\item[\texttt{why3replayer}] replay the proofs stored in a session,
for regression test purposes
\item[\texttt{why3replayer}] replays the proofs stored in a session,
for regression test purposes.
\item[\texttt{why3bench}] produces benchmarks.
\item[\texttt{why3session}] dumps various informations from a proof
session, and possibly modifies the session.
......@@ -19,7 +19,7 @@ provided by the \why environment. These are as follows:
\end{description}
All these tools accept a common subset of command-line options. In
particular the option \verb|-help| which displays the usage and options.
particular, option \verb|-help| displays the usage and options.
\begin{description}
\item[\texttt{-L \textsl{<dir>}}]
adds \texttt{\textsl{<dir>}} in the load path, to search for theories.
......@@ -76,7 +76,7 @@ of the \why data directory (\eg{}
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
tracking system).
tracking system.)
The result of provers detection is stored in the user's
configuration file (\verb+~/.why3.conf+ or, in the case of local
......@@ -353,14 +353,14 @@ are groups together under several tabs
\begin{description}
\item[\textsf{General Settings} tab] This tab allows one to set
variours general settings.
various general settings.
\begin{itemize}
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in
parallel.
\item A few display settings:
\begin{itemize}
\item introduce premises: if selected, the goal of the task shownin
\item introduce premises: if selected, the goal of the task shown in
top-right window is displayed after introduction of universally
quantified variables and implications, \eg a goal of the form
$\forall x: t. P \rightarrow Q$ is displayed as
......@@ -707,7 +707,7 @@ The proof statistics given by option \verb|--stats| are as follows:
sub-goals generated by transformations. The respective minimum,
maximum and average time and on average running time is
shown. Beware that these time data are computed on the
goals \emph{where the prover was successfull}.
goals \emph{where the prover was successful}.
\end{itemize}
For example, here are the session statistics produced on the ``hello
......@@ -750,7 +750,7 @@ The specific options are
\item[\texttt{-o \textsl{<dir>}}] indicates where
to produce LaTeX files (default: the session directory).
\item[\texttt{-longtable}] uses the `longtable' environment instead of
'tabular'.
`tabular'.
\item[\texttt{-e \textsl{<elem>}}] produces a table for the given element, which is
either a file, a theory or a root goal. The element must be specified
using its path in dot notation, \eg \verb|file.theory.goal|. The
......
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