Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help 
COQDOC(1)		     General Commands Manual		       COQDOC(1)

NAME
     coqdoc - documentation tool for the Coq proof assistant

SYNOPSIS
     coqdoc [ options ] files

DESCRIPTION
     coqdoc is a documentation tool for the Coq proof assistant.  It creates La-
     TeX  or HTML documents from a set of Coq files.  See the Coq reference man-
     ual for documentation (url below).

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

     --html
	    Select a HTML output.

     --latex
	    Select a LaTeX output.

     --dvi  Select a DVI output.

     --ps   Select a PostScript output.

     --texmacs
	    Select a TeXmacs output.

     --stdout
	    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 in-
	    sert a title like ``Library Foo'' for each file.

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

     --body-only
	    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{doc-
	    ument} (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	directo-
	    ries.

     -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 in-
     dex.html.

     --no-index
	    Do not output the index.

     --multi-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  out-
	    put, 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).

     --no-externals
	    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 http://coq.in-
	    ria.fr/library/).

     --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 (simi-
	    larly 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	--input-
	    enc latin1 --charset iso-8859-1.

     -utf8, --utf8
	    Select  UTF-8  (Unicode)  input files.  It is equivalent to --input-
	    enc utf8 --charset utf-8.  LaTeX  UTF-8  support  can  be  found  at
	    http://www.ctan.org/tex-archive/macros/latex/contrib/supported/uni-
	    code/.

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

SEE ALSO
     The Coq Reference Manual from http://coq.inria.fr/

								       COQDOC(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=coqdoc&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>

home | help