coqdoc man page on DragonFly

Man page or keyword search:  
man Server   44335 pages
apropos Keyword Search (all sections)
Output format
DragonFly logo
[printable version]

coqdoc(1)							     coqdoc(1)

       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.

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

       --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 (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‐

		      * [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 --inpu‐
	      tenc 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 inpu‐

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

       The Coq Reference Manual from

				  April, 2006			     coqdoc(1)

List of man pages available for DragonFly

Copyright (c) for man pages and the logo by the respective OS vendor.

For those who want to learn more, the polarhome community provides shell access and support.

[legal] [privacy] [GNU] [policy] [cookies] [netiquette] [sponsors] [FAQ]
Polarhome, production since 1999.
Member of Polarhome portal.
Based on Fawad Halim's script.
Vote for polarhome
Free Shell Accounts :: the biggest list on the net