Man Linux: Main Page and Category List


       coqdoc - A documentation tool for the Coq proof assistant


       coqdoc [ options ] files


       coqdoc is a documentation tool for the Coq proof assistant.  It creates
       LaTeX or HTML documents from a set of Coq files.  See the Coq reference
       manual for documentation (url below).


   Overall options
       -h     Help.  Will  give  you  the complete list of options accepted by

       --html Select a HTML output.

              Select a LATEX output.

       --dvi  Select a DVI output.

       --ps   Select a PostScript output.

              Select a TeXmacs output.

              Redirect the output to stdout

       -o file,--output file
              Redirect the output into the file file.

       -d dir, --directory dir
              Output files into directory dir  instead  of  current  directory
              (option  -d  does  not change the filename specified with option
              -o, if any).

       -s,  --short
              Do not insert titles for the files. The default behavior  is  to
              insert a title like ``Library Foo'' for each file.

       -t string, --title string
              Set the document title.

              Suppress the header and trailer of the final document. Thus, you
              can insert the resulting document into a larger one.

       -p string, --preamble string
              Insert  some  material  in  the  LATEX  preamble,  right  before
              \begin{document} (meaningless with -html).

       --vernac-file file, --tex-file file
              Considers the file `file' respectively as a .v (or .g) file or a
              .tex file.

       --files-from file
              Read file names to process in file `file' as if they were  given
              on the command line. Useful for program sources split in several

       -q,  --quiet
              Be quiet. Do not print anything except errors.

       -h,  --help
              Give a short summary of the options and exit.

       -v,  --version
              Print the version and exit.

   Index options
       Default behavior is to build an index, for the HTML output  only,  into

              Do not output the index.

              Generate  one  page  for  each  category  and each letter in the
              index, together with a top page index.html.

   Table of contents option
       -toc,  --table-of-contents
              Insert a table of contents. For a LATEX  output,  it  inserts  a
              \tableofcontents  at  the  beginning of the document. For a HTML
              output, it builds a table of contents into toc.html.

   Hyperlinks options
       --glob-from  file
              Make references using Coq globalizations from file  file.  (Such
              globalizations are obtained with Coq option -dump-glob).

              Do not insert links to the Coq standard library.

       --coqlib url
              Set   base   URL  for  the  Coq  standard  library  (default  is

       --coqlib_path dir
              Set the base path where the Coq files are installed,  especially
              style files coqdoc.sty and coqdoc.css.

       -R dir coqdir
              Map  physical  directory  dir  to  Coq  logical directory coqdir
              (similarly to Coq option -R).  Note: option -R only  has  effect
              on  the  files  following  it  on  the command line, so you will
              probably need to put this option first.

   Contents options
       -g,  --gallina
              Do not print proofs.

       -l,  --light
              Light mode. Suppress proofs  (as  with  -g)  and  the  following

                      * [Recursive] Tactic Definition
                      * Hint / Hints
                      * Require
                      * Transparent / Opaque
                      * Implicit Argument / Implicits
                      * Section / Variable / Hypothesis / End

              The  behavior  of  options  -g  and -l can be locally overridden
              using the (* begin show *) ... (* end show *)  environment  (see

   Language options
       Default behavior is to assume ASCII 7 bits input files.

       -latin1,  --latin1
              Select  ISO-8859-1  input  files. It is equivalent to --inputenc
              latin1 --charset iso-8859-1.

       -utf8,  --utf8
              Select  UTF-8  (Unicode)  input  files.  It  is  equivalent   to
              --inputenc  utf8  --charset  utf-8.  LATEX  UTF-8 support can be
              found                                                         at

       --inputenc string
              Give a LATEX input encoding,  as  an  option  to  LATEX  package

       --charset string
              Specify  the  HTML  character  set,  to  be inserted in the HTML


       The Coq Reference Manual from

                                  April, 2006                        coqdoc(1)