The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Coqdoc gets most of the non-trivial color information from .glob files which are generated at compile time. Coqdoc's coloring goes way beyond keywords. For example, inductively defined types (e.g nat) are blue, and constructors (e.g. S) of inductively defined types are dark red.

Without that information, its unlikely that the simple lstcoq.sty mechanism can do much.

You can always grab parts of a coqdoc generated .tex file and put it in a bigger .tex document. I often use the  catchfilebetweentags latex package to automate this process. I put the tags in the .v file as a comment. For example:
https://github.com/aa755/CFGV/blob/master/SSubst.v#L37
This way, you can be sure that Coq snippets in your latex document are well typed in some context (coqdoc warns if it can't find the .glob files)

Hi,

(I’m not sure this is the correct forum to post questions about coqdoc but I couldn’t find a dedicated mailing list for coqdoc — let me know if this should go elsewhere)

coqdoc can render Coq source files in tex, with a very elegant style (both special fonts and colors). I wonder if there is a way to pretty print Coq source within tex documents following the same style.

I found some libraries for the listings package, in particular this one:
https://hal.archives-ouvertes.fr/file/index/docid/594606/filename/lstcoq.sty
It also has nice colors, but it’s not the same style as coqdoc overall, so one cannot use both in the same document.

Thanks,

-- Éric