Commit f1db7914 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove escape-to-tex delimiters from listing definition, since they are not...

Remove escape-to-tex delimiters from listing definition, since they are not used and Hevea breaks on them.
parent f18e24aa
......@@ -55,7 +55,6 @@ commentstyle=\itshape,%
columns=[l]fullflexible,%
sensitive=true,%
morecomment=[s]{(*}{*)},%
escapeinside={*?}{?*},%
keepspaces=true,
literate=%
%{'a}{$\alpha$}{1}%
......
......@@ -228,8 +228,6 @@ we can launch the following command:
> why3 lists.why -T SortedIntList
\end{verbatim}
to see the resulting theory \texttt{SortedIntList}:
\ifhevea
\else
\begin{whycode}
theory SortedIntList
(* use BuiltIn *)
......@@ -258,7 +256,6 @@ theory SortedIntList
prop Le_refl2 = Le_refl *)
end
\end{whycode}
\fi
In conclusion, let us briefly explain the concept of namespaces
in \why. Both \texttt{use} and \texttt{clone} instructions can
......
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