I want to format Coq code using the LaTeX package "lstcoq.sty". It used to work for me a few years ago, but now I get an error message when trying to use it again. The Coq code inserted in the LaTeX file is:
\begin{coq}
Section example.
Variables A B: Type.
Definition pair:Type:=(A*B).
End example.
\end{coq}
It produces the following error message:
! Argument of � has an extra }.
<inserted text>
\par
l.155 End
example.
? h
I've run across a `}' that doesn't seem to match anything.
For example, `\def\a#1{...}' and `\a}' would produce
this error. If you simply proceed now, the `\par' that
I've just inserted will cause me to report a runaway
argument that might be the root of the problem. But if
your `}' was spurious, just type `2' and it will go away.
Dows any body know why and how to fix it?
Thanks in advance.