Commit 0204695f authored by MARCHE Claude's avatar MARCHE Claude

documentation for the new option -e of why3session latex

parent f1d1e9f1
* marks an incompatible change
o new option -e for "why3session latex" allows to specify when to
split tables in parts
version 0.72, May 11, 2012
o [Coq] new tactic "why3" to call external provers as oracles
......@@ -657,7 +657,16 @@ The specific options are
output, with a different layout of the tables.
\item[\texttt{-o <path>}] where
to produce LaTeX files (default: session dir)
\item[\texttt{-longtable}] use 'longtable' environment instead of 'tabular'
\item[\texttt{-longtable}] use 'longtable' environment instead of
\item[\texttt{-e <elem>}] produces a table for element <elem>, which is
either a file, a theory or a root goal. The <elem> must be specified
using its path in dot notation, e.g. \verb|file.theory.goal|. The
file produced is named accordingly,
e.g. \verb|file.theory.goal.tex|. This option can be given several
times to produce several tables in one run. When this option is
given at least once, the default behavior that is to produce one
table per theory is disabled.
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