0

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.

1 Answer 1

0

Solved. I am using Notepad++ which, for some reason, showed "UTF-8" as the encoding for file "lstcoq.sty". Just in case, I changed the encoding to ANSI and then back to UTF-8. Now it works. Has to do with Notepad++ then, not latex nor the package.

2
  • Can you add the information about the OS on which this is running?
    – Yves
    Nov 21 at 7:00
  • Sure. I am using Windows 10 and the Notepad++ version is 8.5.3 (64 bit).
    – Marcus
    Nov 23 at 19:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.