Provided by: coq_8.15.2+dfsg-2_amd64 bug


       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


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

       --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 directories.

       -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 index.html.

              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.

       --external url libroot
              Set base URL for the external library whose root prefix is libroot.

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

       --coqlib 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 commands:

                      * [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 above).

   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

       -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 inputenc.

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


       The Coq Reference Manual from