Commit 90a9ab7a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Hide from hevea the extraneous space used to workaround a bug in latex.

parent 5f92d65f
......@@ -44,15 +44,15 @@ using the \texttt{timelimit} keyword.
\paragraph{Error messages.} The following errors may be reported by
the Coq tactic.
\item[\texttt{Not a first order goal}] ~\par
\item[\texttt{Not a first order goal}]\emptyitem
The Coq goal could not be translated to \why's logic.
\item[\texttt{Timeout}] ~\par
There was no answer from the prover within the given time limit.
\item[\texttt{Don't know}] ~\par
\item[\texttt{Don't know}]\emptyitem
The prover stopped without validating the goal.
\item[\texttt{Invalid}] ~\par
The prover stopped, reporting the goal to be invalid.
\item[\texttt{Failure}] ~\par
The prover failed. Depending on the message that follows, you may
want to file a bug report, either to the \why\ developers or to the
prover developers.
......@@ -6,6 +6,8 @@
% BNF grammar
......@@ -314,7 +314,7 @@ changed are marked obsolete.
\item[Menu \textsf{File}]~
\item[Menu \textsf{File}]\emptyitem
\item[Add File] adds a file in the GUI.
%\item[Detect provers] runs provers auto-detection
......@@ -325,7 +325,7 @@ changed are marked obsolete.
\item[Quit] exits the GUI.
\item[Menu \textsf{View}]~
\item[Menu \textsf{View}]\emptyitem
\item[Expand All] expands all the rows of the tree view.
\item[Collapse proved goals] closes all the rows of the tree view
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