使用LaTeX的lstcoq.sty包格式化Coq代码报错，求解决方法

错误原因 #

旧版lstcoq.sty包未适配新版LaTeX环境（尤其是listings包的更新），其对Coq关键字（如End）的解析逻辑存在缺陷，错误地将后续内容识别为命令参数，导致括号匹配异常，触发编译错误。该包长期缺乏维护，兼容性问题随LaTeX生态更新逐渐显现。

解决办法 #

方案1：使用Coq官方工具coqdoc（推荐） #

Coq自带的coqdoc工具可直接将.v格式的Coq代码转换为带语法高亮的LaTeX代码，兼容性拉满：

1. 把你的Coq代码保存为example.v文件：

   Section example.
   Variables A B: Type.
   Definition pair:Type:=(A*B).
   End example.
   

2. 执行命令生成LaTeX文件：

   coqdoc -o coq_code.tex example.v
   

3. 在主LaTeX文件中引入生成的代码：

   \input{coq_code.tex}
   

方案2：手动用listings包配置Coq语法 #

如果不想依赖外部工具，可直接在LaTeX中自定义Coq语法规则，替代老旧的lstcoq.sty：

\usepackage{listings}
\usepackage{xcolor} % 用于语法高亮颜色定义

\lstdefinelanguage{Coq}{
  keywords={Section, Variables, Definition, End, Type},
  sensitive=true,
  commentstyle=\itshape\color{gray!60},
  keywordstyle=\bfseries\color{blue!80},
  identifierstyle=\color{black},
  stringstyle=\color{purple!80},
  literate=
    {->}{$\rightarrow$}{2}
    {=>}{$\Rightarrow$}{2}
    {<>}{$\neq$}{2}
    {<=}{$\leq$}{2}
    {>=}{$\geq$}{2},
}

% 使用示例
\begin{lstlisting}[language=Coq]
Section example.
Variables A B: Type.
Definition pair:Type:=(A*B).
End example.
\end{lstlisting}

方案3：修复旧版lstcoq.sty #

若坚持使用该包，可尝试修改其源码：

1. 打开lstcoq.sty文件，找到定义Coq语言的\lstdefinelanguage块。
2. 检查End关键字的定义，确保其不会错误捕获后续内容作为参数。例如，调整关键字的分隔规则，避免将空格后的文本误判为命令参数。
3. 若找不到最新维护版本，可尝试替换其中的listings相关配置为当前兼容的写法。

附：原问题中的代码与错误信息 #

插入的Coq代码：

\begin{coq}
Section example.
Variables A B: Type.
Definition pair:Type:=(A*B).
End example.
\end{coq}

编译错误信息：

! Argument of � has an extra }.

\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.

内容的提问来源于stack exchange，提问作者Marcus