12 files changed, 1148 insertions, 0 deletions
diff --git a/man/coq-tex.1 b/man/coq-tex.1
new file mode 100644
index 0000000000..7e0a2f81e2
--- /dev/null
+++ b/man/coq-tex.1
@@ -0,0 +1,125 @@
+.TH COQ-TEX 1 "29 March 1995"
+
+.SH NAME
+coq-tex \- Process Coq phrases embedded in LaTeX files
+
+.SH SYNOPSIS
+.B coq-tex
+[
+.BI \-o \ output-file
+]
+[
+.BI \-n \ line-width
+]
+[
+.BI \-image \ coq-image
+]
+[
+.B \-w
+]
+[
+.B \-v
+]
+[
+.B \-sl
+]
+[
+.B \-hrule
+]
+[
+.B \-small
+]
+.I input-file ...
+
+
+.SH DESCRIPTION
+
+The
+.B coq-tex
+filter extracts Coq phrases embedded in LaTeX files, evaluates
+them, and insert the outcome of the evaluation after each phrase.
+
+Three LaTeX environments are provided to include Coq code in
+the input files:
+.TP
+.B coq_example
+The phrases between \\begin{coq_example} and \\end{coq_example} are
+evaluated and copied into the output file. Each phrase is followed by
+the response of the toplevel loop.
+.TP
+.B coq_example*
+The phrases between \\begin{coq_example*} and \\end{coq_example*} are
+evaluated and copied into the output file. The responses of the
+toplevel loop are discarded.
+.TP
+.B coq_eval
+The phrases between \\begin{coq_eval} and \\end{coq_eval} are
+silently evaluated. They are not copied into the output file, and the
+responses of the toplevel loop are discarded.
+.PP
+The resulting LaTeX code is stored in the file
+.IR file \&.v.tex
+if the input file has a name of the form
+.IR file \&.tex,
+otherwise the name of the output file is the name of the input file
+with `.v.tex' appended.
+
+The files produced by
+.B coq-tex
+can be directly processed by LaTeX. 
+Both the Coq phrases and the toplevel output are typeset in
+typewriter font.
+
+.SH OPTIONS
+
+.TP
+.BI \-o \ output-file
+Specify the name of a file where the LaTeX output is to be stored. A
+dash `\-' causes the LaTeX output to be printed on standard output.
+.TP
+.BI \-n \ line-width
+Set the line width. The default is 72 characters. The responses of the
+toplevel loop are folded if they are longer than the line width. No
+folding is performed on the Coq input text.
+.TP
+.BI \-image \ coq-image
+Cause the file
+.IR coq-image
+to be executed to evaluate the Coq phrases. By default,
+this is the command 
+.IR coqtop
+without specifying any path which is used to evaluate the Coq phrases.
+.TP
+.B \-w
+Cause lines to be folded on a space character whenever possible,
+avoiding word cuts in the output. By default, folding occurs at
+the line width, regardless of word cuts.
+.TP
+.B \-v
+Verbose mode. Prints the Coq answers on the standard output.
+Useful to detect errors in Coq phrases.
+.TP
+.B \-sl
+Slanted mode. The Coq answers are written in a slanted font.
+.TP
+.B \-hrule
+Horizontal lines mode. The Coq parts are written between two
+horizontal lines.
+.TP
+.B \-small
+Small font mode. The Coq parts are written in a smaller font.
+
+
+.SH CAVEATS
+The \\begin... and \\end... phrases must sit on a line by themselves,
+with no characters before the backslash or after the closing brace.
+Each Coq phrase must be terminated by `.' at the end of a line.
+Blank space is accepted between `.' and the newline, but any other
+character will cause coq-tex to ignore the end of the phrase,
+resulting in an incorrect shuffling of the responses into the phrases.
+(The responses ``lag behind''.)
+
+.SH SEE ALSO
+
+.B coqtop
+(1).
diff --git a/man/coq_makefile.1 b/man/coq_makefile.1
new file mode 100644
index 0000000000..b5de6d367d
--- /dev/null
+++ b/man/coq_makefile.1
@@ -0,0 +1,33 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq_makefile \- The Coq Proof Assistant makefile generator
+
+
+.SH SYNOPSIS
+.B coq_makefile
+[
+.B arguments
+]
+
+.SH DESCRIPTION
+
+.B coq_makefile
+is a makefile generator for Coq proof developments.
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Will give you a description of the whole list of options of coq_makefile.
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqtc (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coqc.1 b/man/coqc.1
new file mode 100644
index 0000000000..1e597afd99
--- /dev/null
+++ b/man/coqc.1
@@ -0,0 +1,64 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqc \- The Coq Proof Assistant compiler
+
+
+.SH SYNOPSIS
+.B coqc
+[
+.B general \ Coq \ options
+]
+.I file
+
+
+.SH DESCRIPTION
+
+.B coqc
+is the batch compiler for the Coq Proof Assistant.
+The options are basically the same as coqtop(1).
+.IR file.v \&
+is the vernacular file to compile.
+.IR file \& 
+must be formed
+only with the characters `a` to  `Z`, `0`-`9` or `_` and must begin
+with a letter.
+The compiler produces an object file
+.IR file.vo \&.
+
+For interactive use of Coq, see 
+.BR coqtop(1).
+
+
+.SH OPTIONS
+
+.B coqc
+is a script that simply runs
+.B coqtop
+with option 
+.B \-compile
+it accepts the same options as
+.B coqtop.
+
+.TP
+.BI \-image \ bin
+use
+.I bin
+as underlying
+.B coqtop
+instead of the default one.
+
+.TP
+.BI \-verbose
+print the compiled file on the standard output.
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coq_makefile (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coqchk.1 b/man/coqchk.1
new file mode 100644
index 0000000000..f9241c0d47
--- /dev/null
+++ b/man/coqchk.1
@@ -0,0 +1,101 @@
+.TH COQ 1 "July 7, 201"
+
+.SH NAME
+coqchk \- The Coq Proof Checker compiled libraries verifier
+
+
+.SH SYNOPSIS
+.B coqchk
+[
+.B options
+]
+.I modules
+
+
+.SH DESCRIPTION
+
+.B coqchk
+is the standalone checker of compiled libraries (.vo files produced by
+coqc) for the Coq Proof Assistant. See the Reference Manual for more
+information. It returns with exit code 0 if all the requested tasks
+succeeded. A non-zero return code means that something went wrong: some
+library was not found, corrupted content, type-checking failure, etc.
+
+.IR modules \&
+is a list of modules to be checked. Modules can be referred to by a
+short or qualified logical name, or by their filename.
+
+.SH OPTIONS
+
+.TP
+.BI \-I \ dir, \ \-\-include \ dir
+add directory 
+.I dir
+in the include path
+
+.TP
+.BI \-Q \ dir\ coqdir
+map physical
+.I dir
+to logical
+.I coqdir
+
+.TP
+.BI \-R \ dir\ coqdir
+synonymous for -Q
+
+.TP
+.BI \-silent
+makes coqchk less verbose.
+
+.TP
+.BI \-admit \ module
+tag the specified module and all its dependencies as trusted, and will
+not be rechecked, unless explicitly requested by other options.
+
+.TP
+.BI \-norec \ module
+specifies that the given module shall be verified without requesting
+to check its dependencies.
+
+.TP
+.BI \-m,\ \-\-memory
+displays a summary of the memory used by the checker.
+
+.TP
+.BI \-o,\ \-\-output\-context
+displays a summary of the logical content that have been
+verified: assumptions and usage of impredicativity.
+
+.TP
+.BI \-impredicative\-set
+allows the checker to accept libraries that have been compiled with
+this flag.
+
+.TP
+.BI \-v
+print coqchk version and exit.
+
+.TP
+.BI \-coqlib \ dir
+overrides the default location of the standard library.
+
+.TP
+.BI \-where
+print coqchk standard library location and exit.
+
+.TP
+.BI \-h,\ \-\-help
+print list of options
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqc (1),
+.BR coq_makefile (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coqdep.1 b/man/coqdep.1
new file mode 100644
index 0000000000..c417402c25
--- /dev/null
+++ b/man/coqdep.1
@@ -0,0 +1,206 @@
+.TH COQ 1 "28 March 1995" "Coq tools"
+
+.SH NAME
+coqdep \- Compute inter-module dependencies for Coq and Caml programs
+
+.SH SYNOPSIS
+.B coqdep
+[
+.BI \-w
+]
+[
+.BI \-I \ directory
+]
+[
+.BI \-coqlib \ directory
+]
+[
+.BI \-c
+]
+[
+.BI \-i
+]
+[
+.BI \-D
+]
+[
+.BI \-slash
+]
+.I filename ...
+.I directory ...
+
+.SH DESCRIPTION
+
+.B coqdep
+compute inter-module dependencies for Coq and Caml programs,
+and prints the dependencies on the standard output in a format
+readable by make.
+When a directory is given as argument, it is recursively looked at.
+
+Dependencies of Coq modules are computed by looking at
+.IR Require \&
+commands (Require, Require Export, Require Import),
+.IR Declare \& 
+.IR ML \& 
+.IR Module \&
+commands and
+.IR Load \&
+commands. Dependencies relative to modules from the Coq library are not
+printed except if 
+.BR \-boot \&
+is given.
+
+Dependencies of Caml modules are computed by looking at
+.IR open \&
+directives and the dot notation
+.IR module.value \&.
+
+.SH OPTIONS
+
+.TP
+.BI \-c
+Prints the dependencies of Caml modules.
+(On Caml modules, the behaviour is exactly the same as ocamldep).
+\" THESE OPTIONS ARE BROKEN CURRENTLY
+\" .TP
+\" .BI \-w
+\" Prints a warning if a Coq command
+\" .IR Declare \& 
+\" .IR ML \& 
+\" .IR Module \&
+\" is incorrect. (For instance, you wrote `Declare ML Module "A".',
+\" but the module A contains #open "B"). The correct command is printed
+\" (see option \-D). The warning is printed on standard error.
+\" .TP
+\" .BI \-D
+\" This commands looks for every command
+\" .IR Declare \& 
+\" .IR ML \& 
+\" .IR Module \&
+\" of each Coq file given as argument and complete (if needed)
+\" the list of Caml modules. The new command is printed on
+\" the standard output. No dependency is computed with this option.
+.TP
+.BI \-f \ file
+Read filenames and options -I, -R and -Q from a _CoqProject FILE.
+.TP 
+.BI \-I/\-Q/\-R \ options
+Have the same effects on load path and modules names as for other
+coq commands (coqtop, coqc).
+.TP 
+.BI \-coqlib \ directory
+Indicates where is the Coq library. The default value has been
+determined at installation time, and therefore this option should not
+be used under normal circumstances.
+.TP 
+.BI \-dumpgraph[box] \ file
+Dumps a dot dependency graph in file
+.IR file \&.
+.TP 
+.BI \-exclude-dir \ dir
+Skips subdirectory
+.IR dir \ during
+.BR -R/-Q \ search.
+.TP 
+.B \-sort
+Output the given file name ordered by dependencies.
+.TP 
+.B \-boot
+For coq developpers, prints dependencies over coq library files
+(omitted by default).
+
+
+.SH SEE ALSO
+
+.BR ocamlc (1),
+.BR coqc (1),
+.BR make (1).
+.br
+
+.SH NOTES
+
+Lexers (for Coq and Caml) correctly handle nested comments
+and strings.
+
+The treatment of symbolic links is primitive.
+
+If two files have the same name, in two different directories,
+a warning is printed on standard error.
+
+There is no way to limit the scope of the recursive search for
+directories.
+
+.SH EXAMPLES
+
+.LP
+Consider the files (in the same directory):
+
+	A.ml B.ml C.ml D.ml X.v Y.v and Z.v
+
+where
+.TP
+.BI \+ 
+D.ml contains the commands `open A', `open B' and `type t = C.t' ;
+.TP
+.BI \+
+Y.v contains the command `Require X' ;
+.TP
+.BI \+
+Z.v contains the commands `Require X' and `Declare ML Module "D"'.
+.LP
+To get the dependencies of the Coq files:
+.IP
+.B
+example% coqdep \-I . *.v
+.RS
+.sp .5
+.nf
+.B Z.vo: Z.v ./X.vo ./D.cmo
+.B Y.vo: Y.v ./X.vo
+.B X.vo: X.v
+.fi
+.RE
+.br
+.ne 7
+.LP
+With a warning:
+.IP
+.B
+example% coqdep \-w \-I . *.v
+.RS
+.sp .5
+.nf
+.B Z.vo: Z.v ./X.vo ./D.cmo
+.B Y.vo: Y.v ./X.vo
+.B X.vo: X.v
+### Warning : In file Z.v, the ML modules declaration should be
+### Declare ML Module "A" "B" "C" "D".
+.fi
+.RE
+.br
+.ne 7
+.LP
+To get only the Caml dependencies:
+.IP
+.B
+example% coqdep \-c \-I . *.ml
+.RS
+.sp .5
+.nf
+.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
+.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
+.B C.cmo: C.ml
+.B C.cmx: C.ml
+.B B.cmo: B.ml
+.B B.cmx: B.ml
+.B A.cmo: A.ml
+.B A.cmx: A.ml
+.fi
+.RE
+.br
+.ne 7
+
+.SH BUGS
+
+Please report any bug to
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/coqdoc.1 b/man/coqdoc.1
new file mode 100644
index 0000000000..8d71a8746d
--- /dev/null
+++ b/man/coqdoc.1
@@ -0,0 +1,190 @@
+.TH coqdoc 1 "April, 2006"
+
+.SH NAME
+coqdoc \- A documentation tool for the Coq proof assistant
+
+
+.SH SYNOPSIS
+.B coqdoc
+[
+.B options
+]
+.B files
+
+
+.SH DESCRIPTION
+
+.B 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).
+
+
+.SH OPTIONS
+
+.SS Overall options
+
+.TP
+.BI \-h
+Help. Will give you the complete list of options accepted by coqdoc.
+.TP
+.B \-\-html
+Select a HTML output.
+.TP
+.B \-\-latex
+Select a LATEX output.
+.TP
+.B \-\-dvi
+Select a DVI output.
+.TP
+.B \-\-ps
+Select a PostScript output.
+.TP
+.B \-\-texmacs
+Select a TeXmacs output.
+.TP
+.B \-\-stdout
+Redirect the output to stdout
+.TP
+.BI \-o \ file, \-\-output \ file
+Redirect the output into the file 
+.I file.
+.TP
+.BI \-d \ dir, \ \-\-directory \ dir
+Output files into directory 
+.I dir 
+instead of current directory (option
+\-d does not change the filename specified with option \-o, if any).
+.TP
+.B \-s, \ \-\-short
+Do not insert titles for the files. The default behavior is to insert
+a title like ``Library Foo'' for each file.
+.TP
+.BI \-t \ string, \ \-\-title \ string
+Set the document title.
+.TP
+.B \-\-body\-only
+Suppress the header and trailer of the final document. Thus, you can
+insert the resulting document into a larger one.
+.TP
+.BI \-p \ string, \ \-\-preamble \ string
+Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
+.TP
+.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
+Considers the file `file' respectively as a .v (or .g) file or a .tex file.
+.TP
+.BI \-\-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.
+.TP
+.B \-q, \ \-\-quiet
+Be quiet. Do not print anything except errors.
+.TP
+.B \-h, \ \-\-help
+Give a short summary of the options and exit.
+.TP
+.B
+\-v, \ \-\-version
+Print the version and exit.
+
+.SS Index options
+
+Default behavior is to build an index, for the HTML output only, into
+index.html.
+
+.TP
+.B \-\-no\-index
+Do not output the index.
+.TP
+.B \-\-multi\-index
+Generate one page for each category and each letter in the index,
+together with a top page index.html.
+
+.SS Table of contents option
+ 
+.TP
+.B \-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.
+
+.SS Hyperlinks options
+
+.TP
+.B \-\-glob\-from \ file
+Make references using Coq globalizations from file file. (Such
+globalizations are obtained with Coq option \-dump\-glob).
+
+.TP
+.B \-\-no\-externals
+Do not insert links to the Coq standard library.
+
+.TP
+.BI \-\-external \ url \  libroot
+Set base URL for the external library whose root prefix is libroot.
+
+.TP
+.BI \-\-coqlib \ url
+Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
+
+.TP
+.BI \-\-coqlib_path \ dir
+Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
+
+.TP
+.BI \-R \ dir \  coqdir
+Map physical directory dir to Coq logical directory coqdir (similarly
+to Coq option \-R).
+.B 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.
+
+.SS Contents options
+
+.TP
+.B \-g, \ \-\-gallina
+Do not print proofs.
+
+.TP
+.B \-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).
+
+.SS Language options
+ 
+Default behavior is to assume ASCII 7 bits input files.
+
+.TP 
+.B \-latin1, \ \-\-latin1
+Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
+\-\-charset iso\-8859\-1.
+
+.TP 
+.B \-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/contrib/supported/unicode/.
+
+.TP 
+.BI \-\-inputenc \ string
+Give a LATEX input encoding, as an option to LATEX package inputenc.
+
+.TP
+.BI \-\-charset \ string
+Specify the HTML character set, to be inserted in the HTML header.
+
+
+.SH SEE ALSO
+
+.I
+The Coq Reference Manual from http://coq.inria.fr/
+
diff --git a/man/coqide.1 b/man/coqide.1
new file mode 100644
index 0000000000..3592f6e4e3
--- /dev/null
+++ b/man/coqide.1
@@ -0,0 +1,143 @@
+.TH COQIDE 1 "July 16, 2004"
+
+.SH NAME
+coqide \- The Coq Proof Assistant graphical interface
+
+
+.SH SYNOPSIS
+.B coqide
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqide
+is a gtk graphical interface for the Coq proof assistant.
+
+For command-line-oriented use of Coq, see
+.BR coqtop (1)
+; for batch-oriented use of Coq, see 
+.BR coqc (1).
+
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Show the complete list of options accepted by
+.BR coqide .
+.TP
+.BI \-I\  dir ,\ \-include\  dir
+Add directory dir in the include path.
+.TP
+.BI \-R\  dir\ coqdir
+Recursively map physical
+.I dir
+to logical
+.IR coqdir .
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-load\-ml\-object\  f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\  f
+Load ML file
+.IR f .
+.TP
+.BI \-l\  f ,\ \-load\-vernac\-source\  f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\  path
+Load Coq library
+.IR path
+(Require
+.IR path .).
+.TP
+.BI \-require\  path
+Load Coq library
+.IR path
+and import it (Require Import
+.IR path .).
+.TP
+.BI \-compile\  f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\  f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR -batch ).
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B -v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\  f
+Set the rcfile to
+.IR f .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\  f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coqtop (1),
+.BR coq-tex (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual,
+.I
+The Coq web site: http://coq.inria.fr,
+.I
+/usr/share/doc/coqide/FAQ.
+
+.SH AUTHOR
+This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
+for the Debian project (but may be used by others).
diff --git a/man/coqtop.1 b/man/coqtop.1
new file mode 100644
index 0000000000..084adfe453
--- /dev/null
+++ b/man/coqtop.1
@@ -0,0 +1,159 @@
+.TH COQ 1 "October 11, 2006"
+
+.SH NAME
+coqtop \- The Coq Proof Assistant toplevel system
+
+
+.SH SYNOPSIS
+.B coqtop
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is the toplevel system of Coq, for interactive use.
+It reads phrases on the standard input, and prints results on the
+standard output.
+
+For batch-oriented use of Coq, see 
+.BR coqc(1).
+
+
+.SH OPTIONS
+
+.TP
+.B \-h, \-\-help
+Help. Will give you the complete list of options accepted by coqtop.
+
+.TP
+.BI \-I \ dir, \ \-\-include \ dir
+add directory 
+.I dir
+in the include path
+
+.TP
+.BI \-R \ dir\ coqdir          
+recursively map physical
+.I dir
+to logical
+.I coqdir
+
+.TP
+.BI \-top \ coqdir
+set the toplevel name to be
+.I coqdir
+instead of Top
+
+.TP
+.B \-nois
+start with an empty initial state
+
+.TP
+.BI \-load\-ml\-object \ filename
+load ML object file
+.I filenname
+
+.TP
+.BI \-load\-ml\-source \ filename
+load ML file
+.I filename
+
+.TP
+.BI \-load\-vernac\-source \ filename, \ \-l \ filename
+load Coq file
+.I filename.v
+(Load filename.)
+
+.TP
+.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename 
+load verbosely Coq file
+.I filename.v
+(Load Verbose filename.)
+
+.TP
+.BI \-load\-vernac\-object \ path
+load Coq library
+.I path
+(Require path.)
+
+.TP
+.BI \-require \ path
+load Coq library
+.I path
+and import it (Require Import path.)
+
+.TP
+.BI \-compile \ filename.v
+compile Coq file
+.I filename.v 
+(implies 
+.B \-batch
+)
+
+.TP
+.BI \-compile\-verbose \ filename.v
+verbosely compile Coq file
+.I filename.v
+(implies 
+.B \-batch
+)
+
+.TP
+.B \-where
+print Coq's standard library location and exit
+
+.TP
+.B \-v
+print Coq version and exit
+
+.TP
+.B \-q
+skip loading of rcfile (resource file) if any
+
+.TP
+.BI \-init\-file \ filename
+set the rcfile to
+.I filename
+
+.TP
+.B \-batch
+batch mode (exits just after arguments parsing)
+
+.TP
+.B \-boot
+boot mode (implies
+.B \-q
+and
+.B \-batch
+)
+
+.TP
+.B \-emacs
+tells Coq it is executed under Emacs
+
+.TP
+.BI \-dump\-glob \ filename
+dump globalizations in file f (to be used by
+.B coqdoc(1)
+)
+
+.TP
+.B \-impredicative\-set
+set sort Set impredicative
+
+.TP
+.B \-dont\-load\-proofs
+don't load opaque proofs in memory
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coq-tex (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1
new file mode 100644
index 0000000000..ad1a358c32
--- /dev/null
+++ b/man/coqtop.byte.1
@@ -0,0 +1,35 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqtop.byte \- The bytecode Coq toplevel
+
+
+.SH SYNOPSIS
+.B coqtop.byte
+[
+.B options
+]
+[
+.I file
+]
+
+.SH DESCRIPTION
+
+.B coqopt.byte
+is the bytecode version of Coq. It should not be called directly, but
+only by
+.B coqtop
+and
+.B coqc
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqc (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
+
+
diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1
new file mode 100644
index 0000000000..17c763da33
--- /dev/null
+++ b/man/coqtop.opt.1
@@ -0,0 +1,35 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqtop.opt \- The native-code Coq toplevel
+
+
+.SH SYNOPSIS
+.B coqopt.opt
+[
+.B options
+]
+[
+.I file
+]
+
+.SH DESCRIPTION
+
+.B coqopt.opt
+is the native-code version of Coq. It should not be called directly, but
+only by
+.B coqtop
+and
+.B coqc
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqc (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
+
+
diff --git a/man/coqwc.1 b/man/coqwc.1
new file mode 100644
index 0000000000..4594aeecb7
--- /dev/null
+++ b/man/coqwc.1
@@ -0,0 +1,47 @@
+.TH COQ 1 "16 March 2004" "Coq tools"
+
+.SH NAME
+coqwc \- print the number of specification, proof and comment lines in
+Coq files
+
+.SH SYNOPSIS
+.B coqwc
+[
+.BI \-p
+]
+[
+.BI \-s
+]
+[
+.BI \-r
+]
+[
+.BI \-e
+]
+.I files ...
+
+.SH DESCRIPTION
+
+.B coqwc
+computes the number of specification lines, proof lines and comment
+lines in Coq files.
+
+.SH OPTIONS
+
+.TP
+.BI \-p
+Print the percentage of comments
+.TP
+.BI \-s
+Print only the number of specification lines
+.TP
+.BI \-r
+Print only the number of proof lines
+.TP
+.BI \-e
+Do not skip headers
+
+.SH BUGS
+
+Please report any bug to
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/dune b/man/dune
new file mode 100644
index 0000000000..359e780545
--- /dev/null
+++ b/man/dune
@@ -0,0 +1,10 @@
+(install
+ (section man)
+ (package coq)
+ (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1))
+
+(install
+ (section man)
+ (package coqide)
+ (files coqide.1))
+