Hi all, I've recently updated my texlive package on Debian unstable (to version 2022.20220722-1) and now I'm getting weird errors from test-suite/coq-makefile/latex1.v.
I get a bunch of
! Argument of <C2> has an extra }.
<inserted text>
\par
l.24 ...t.sub.testsub}{Library }{test.sub.testsub}
Runaway argument?
Did I break something in my installation, or is the Coq tex wrapper incompatible with the latest TexLive release?
I'll see if coq-doc compiles with a recent unstable -- I didn't check that when I did my Coq 8.16 work
The compilation of coq-doc 8.15.2 just went through. [Reminder: coq-doc is the non-free package building the Coq documentation in Debian]
Last updated: Dec 07 2023 at 07:39 UTC