The Coq mailing list

[Éric Tanter <etanter AT dcc.uchile.cl>]

On 23-05-2015, at 12:22, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
[...]

You can always grab parts of a coqdoc generated .tex file and put it in a bigger .tex document.

Yes, that's what I have been doing but manually... Not very nice.

I often use the  catchfilebetweentags latex package to automate this process. I put the tags in the .v file as a comment.

This is cool, thanks! I didn't know about this package.

-- Éric