Imported Upstream version 8.0pl1upstream/8.0pl1

13 files changed, 760 insertions, 0 deletions

diff --git a/man/coq-interface.1 b/man/coq-interface.1
new file mode 100644
index 00000000..2ab2bf95
--- /dev/null
+++ b/man/coq-interface.1
@@ -0,0 +1,37 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq-interface \-
+
+
+.SH SYNOPSIS
+.B coq-interface
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coq-interface
+is a Coq customized toplevel system for Coq containing some modules
+useful for the graphical interface. This program is not for the casual
+user.
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Help. Will give you the complete list of options accepted by
+coq-interface (the same as coqtop).
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coqdep (1),
+.BR coqtop (1),
+.BR parser (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coq-tex.1 b/man/coq-tex.1
new file mode 100644
index 00000000..737de70a
--- /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 00000000..b5de6d36
--- /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 00000000..741b3dcb
--- /dev/null
+++ b/man/coqc.1
@@ -0,0 +1,49 @@
+.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
+
+.TP
+.BI \-h
+Will give you a description of the whole list of options of coqc and
+coqtop.
+
+.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/coqdep.1 b/man/coqdep.1
new file mode 100644
index 00000000..01d080fc
--- /dev/null
+++ b/man/coqdep.1
@@ -0,0 +1,182 @@
+.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
+]
+.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, Require Implementation),
+and
+.IR Declare \& 
+.IR ML \& 
+.IR Module \&
+commands. Dependencies relative to modules from the Coq library are not
+printed.
+
+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 cldepend,
+except that nested comments and strings are correctly handled).
+.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 \-i
+Prints also the dependencies for .vi files (Coq specification modules).
+.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 \-I \ directory
+The files .v .ml .mli of the directory
+.IR directory \&
+are taken into account during the calculus of dependencies,
+but their own dependencies are not printed.
+.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.
+
+
+.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.zo
+.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.zo
+.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.zo: D.ml ./A.zo ./B.zo ./C.zo
+.B C.zo: C.ml
+.B B.zo: B.ml
+.B A.zo: 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 00000000..c325d221
--- /dev/null
+++ b/man/coqdoc.1
@@ -0,0 +1,33 @@
+.TH coqdoc 1 "February, 2002"
+
+.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
+
+.TP
+.B \-h
+Help. Will give you the complete list of options accepted by coqdoc.
+
+
+.SH SEE ALSO
+
+.I
+The Coq web site: http://coq.inria.fr/
diff --git a/man/coqmktop.1 b/man/coqmktop.1
new file mode 100644
index 00000000..05e73d75
--- /dev/null
+++ b/man/coqmktop.1
@@ -0,0 +1,41 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqmktop \- The Coq Proof Assistant user-tactics linker
+
+
+.SH SYNOPSIS
+.B coqmktop
+[
+.I options
+]
+.I files
+
+
+.SH DESCRIPTION
+
+.B coqmktop
+builds a new Coq toplevel extended with user-tactics.
+.IR files \&
+are the Objective Caml object or library files (i.e. with suffix .cmo,
+.cmx, .cma or .cmxa) to link with the Coq system.
+The linker produces an executable Coq toplevel which can be called
+directly or through coqc(1), using the -image option.
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Help. List the available options.
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR ocamlmktop (1).
+.BR ocamlc (1).
+.BR ocamlopt (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coqtop.1 b/man/coqtop.1
new file mode 100644
index 00000000..d75b283f
--- /dev/null
+++ b/man/coqtop.1
@@ -0,0 +1,39 @@
+.TH COQ 1 "April 25, 2001"
+
+.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. Will give you the complete list of options accepted by coqtop.
+
+.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 00000000..ad1a358c
--- /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 00000000..17c763da
--- /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 00000000..7011d148
--- /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/gallina.1 b/man/gallina.1
new file mode 100644
index 00000000..8c607216
--- /dev/null
+++ b/man/gallina.1
@@ -0,0 +1,74 @@
+.TH COQ 1 "29 March 1995" "Coq tools"
+
+.SH NAME
+gallina \- extracts specification from Coq vernacular files
+
+.SH SYNOPSIS
+.B gallina
+[
+.BI \-
+]
+[
+.BI \-stdout
+]
+[
+.BI \-nocomments
+]
+.I file ...
+
+.SH DESCRIPTION
+
+.B gallina 
+takes Coq files as arguments and builds the corresponding
+specification files.
+The Coq file
+.IR foo.v \&
+gives bearth to the specification file
+.IR foo.g. \&
+The suffix '.g' stands for Gallina.
+
+For that purpose, gallina removes all commands that follow a
+"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it
+reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof
+<...>.". It also removes every "Hint", "Syntax",
+"Immediate"  or "Transparent" command.
+
+Files without the .v suffix are ignored.
+
+
+.SH OPTIONS
+
+.TP
+.BI \-stdout
+Prints the result on standard output.
+.TP
+.BI \-
+Coq source is taken on standard input. The result is printed on
+standard output.
+.TP
+.BI \-nocomments
+Comments are removed in the *.g file.
+
+.SH NOTES
+
+Nested comments are correctly handled. In particular, every command
+"Save." or "Abort." in a comment is not taken into account.
+
+
+.SH BUGS
+
+Please report any bug to
+.B coq@pauillac.inria.fr
+
+
+
+
+
+
+	
+
+	
+
+	
+
+	
diff --git a/man/parser.1 b/man/parser.1
new file mode 100644
index 00000000..d89465d8
--- /dev/null
+++ b/man/parser.1
@@ -0,0 +1,30 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+parser \- Coq parser
+
+
+.SH SYNOPSIS
+.B parser
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B parser
+is a program reading Coq proof developments and outputing them in the
+structured format given in the INRIA technical report RT154. This
+program is not for the casual user.
+
+.SH SEE ALSO
+
+.BR coq-interface (1),
+.BR coqc (1),
+.BR coqtop (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr