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
       LaTeX or	HTML documents from a set of Coq files.	 See the Coq reference
       manual for documentation	(url below).

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

       --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
	      insert 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  \be-
	      gin{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.

       --no-index
	      Do not output the	index.

       --multi-index
	      Generate one page	for each category and each letter in  the  in-
	      dex, 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).

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

       --coqlib_url url
	      Set   base   URL	for  the  Coq  standard	 library  (default  is
	      http://coq.inria.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 (sim-
	      ilarly  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  com-
	      mands:

	      •	 [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 us-
	      ing 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
	      --inputenc utf8  --charset utf-8.	  LaTeX	 UTF-8	support	can be
	      found    at    http://www.ctan.org/tex-archive/macros/latex/con-
	      trib/supported/unicode/.

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

home | help