# Article latex document class out of a Coq script

**URL:** <https://discourse.rocq-prover.org/t/article-latex-document-class-out-of-a-coq-script/1042>\
**Category:** Using Rocq\
**Created:** [September 6, 2020, 7:37pm UTC](https://discourse.rocq-prover.org/t/article-latex-document-class-out-of-a-coq-script/1042 "2020-09-06T19:37:43Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![flaviodemoura](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/flaviodemoura/32/391_2.png) [@flaviodemoura](https://discourse.rocq-prover.org/u/flaviodemoura)\
**Post date:** [September 6, 2020, 7:37pm UTC](https://discourse.rocq-prover.org/t/article-latex-document-class-out-of-a-coq-script/1042/1 "2020-09-06T19:37:44Z")

</div>

Hi there,

I would like to know if there exists a direct way to generate a pdf out of a Coq script annotated with coqdoc using a given latex document class, like article or llncs. I usually do it by first generating the latex output of the coq script file with coqdoc, and then compiling the latex output separately (after some editing), but this sequence of repetitive steps is a bit annoying.

Best regards,  
Flávio.

---

<div class="post-metadata">

**Author:** ![flaviodemoura](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/flaviodemoura/32/391_2.png) [@flaviodemoura](https://discourse.rocq-prover.org/u/flaviodemoura)\
**Post date:** [September 30, 2020, 9:30pm UTC](https://discourse.rocq-prover.org/t/article-latex-document-class-out-of-a-coq-script/1042/2 "2020-09-30T21:30:16Z")

</div>

Hi there,

This is another question related to the previous one. I usually need to insert a tex file generated from a annotated coq file via coq. Suppose my coq file starts with an introduction section:

> (\*\* \* Introduction \*)

The coqdoc generates the tex file via the command:

> coqdoc --latex --body-only myfile.v

The generated output is as follows:

```
\coqlibrary{myfile}{Library }{myfile}
\begin{coqdoccode}
\coqdocemptyline
\end{coqdoccode}
\section{Introduction}

```

Is it possible to generate the output tex file without these four initial line? I mean, is it possible to generate the output starting with the following line (as in the Coq script)?

> \section{Introduction}

Thank you very much in advance.  
Flávio.

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [September 30, 2020, 10:19pm UTC](https://discourse.rocq-prover.org/t/article-latex-document-class-out-of-a-coq-script/1042/3 "2020-09-30T22:19:09Z")

</div>

Well, you could pipe the ouput of `coqdoc` into the command `tail -n +5` to skip the first 4 lines.