Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg

8 files changed, 210 insertions, 44 deletions

diff --git a/man/coq-interface.1 b/man/coq-interface.1
index 2ab2bf95..ee013d95 100644
--- a/man/coq-interface.1
+++ b/man/coq-interface.1
@@ -1,7 +1,7 @@
 .TH COQ 1 "April 25, 2001"
 
 .SH NAME
-coq-interface \-
+coq\-interface \- Customized Coq toplevel to make user interfaces
 
 
 .SH SYNOPSIS
@@ -29,7 +29,7 @@ coq-interface (the same as coqtop).
 .BR coqc (1),
 .BR coqdep (1),
 .BR coqtop (1),
-.BR parser (1).
+.BR coq\-parser (1).
 .br
 .I
 The Coq Reference Manual.
diff --git a/man/parser.1 b/man/coq-parser.1
index d89465d8..23dc8201 100644
--- a/man/parser.1
+++ b/man/coq-parser.1
@@ -1,11 +1,11 @@
 .TH COQ 1 "April 25, 2001"
 
 .SH NAME
-parser \- Coq parser
+coq\-parser \- Coq parser
 
 
 .SH SYNOPSIS
-.B parser
+.B coq\-parser
 [
 .B options
 ]
@@ -19,7 +19,7 @@ program is not for the casual user.
 
 .SH SEE ALSO
 
-.BR coq-interface (1),
+.BR coq\-interface (1),
 .BR coqc (1),
 .BR coqtop (1),
 .BR coqdep (1).
diff --git a/man/coq-tex.1 b/man/coq-tex.1
index 737de70a..7e0a2f81 100644
--- a/man/coq-tex.1
+++ b/man/coq-tex.1
@@ -15,19 +15,19 @@ coq-tex \- Process Coq phrases embedded in LaTeX files
 .BI \-image \ coq-image
 ]
 [
-.B -w
+.B \-w
 ]
 [
-.B -v
+.B \-v
 ]
 [
-.B -sl
+.B \-sl
 ]
 [
-.B -hrule
+.B \-hrule
 ]
 [
-.B -small
+.B \-small
 ]
 .I input-file ...
 
@@ -75,7 +75,7 @@ typewriter font.
 .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.
+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
@@ -90,23 +90,23 @@ this is the command
 .IR coqtop
 without specifying any path which is used to evaluate the Coq phrases.
 .TP
-.B -w
+.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
+.B \-v
 Verbose mode. Prints the Coq answers on the standard output.
 Useful to detect errors in Coq phrases.
 .TP
-.B -sl
+.B \-sl
 Slanted mode. The Coq answers are written in a slanted font.
 .TP
-.B -hrule
+.B \-hrule
 Horizontal lines mode. The Coq parts are written between two
 horizontal lines.
 .TP
-.B -small
+.B \-small
 Small font mode. The Coq parts are written in a smaller font.
 
 
diff --git a/man/coqdep.1 b/man/coqdep.1
index 6ae89f8b..e2cbb40e 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -67,7 +67,7 @@ Prints a warning if a Coq command
 .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.
+(see option \-D). The warning is printed on standard error.
 .TP
 .BI \-i
 Prints also the dependencies for .vi files (Coq specification modules).
@@ -138,7 +138,7 @@ Z.v contains the commands `Require X' and `Declare ML Module "D"'.
 To get the dependencies of the Coq files:
 .IP
 .B
-example% coqdep -I . *.v
+example% coqdep \-I . *.v
 .RS
 .sp .5
 .nf
@@ -153,7 +153,7 @@ example% coqdep -I . *.v
 With a warning:
 .IP
 .B
-example% coqdep -w -I . *.v
+example% coqdep \-w \-I . *.v
 .RS
 .sp .5
 .nf
@@ -170,7 +170,7 @@ example% coqdep -w -I . *.v
 To get only the Caml dependencies:
 .IP
 .B
-example% coqdep -c -I . *.ml
+example% coqdep \-c \-I . *.ml
 .RS
 .sp .5
 .nf
@@ -190,4 +190,4 @@ example% coqdep -c -I . *.ml
 .SH BUGS
 
 Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index c443e8b0..45fcafd2 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -54,7 +54,7 @@ Redirect the output into the file
 Output files into directory 
 .I dir 
 instead of current directory (option
--d does not change the filename specified with option -o, if any).
+\-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
@@ -68,7 +68,7 @@ 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).
+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.
@@ -114,7 +114,7 @@ it builds a table of contents into toc.html.
 .TP
 .B \-\-glob\-from \ file
 Make references using Coq globalizations from file file. (Such
-globalizations are obtained with Coq option -dump-glob).
+globalizations are obtained with Coq option \-dump\-glob).
 
 .TP
 .B \-\-no\-externals
@@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar
 Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
 
 .TP
-.BI -R \ dir \  coqdir
+.BI \-R \ dir \  coqdir
 Map physical directory dir to Coq logical directory coqdir (similarly
-to Coq option -R).
+to Coq option \-R).
 .B Note: 
-option -R only has effect on the files following it on the command
+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
+.B \-g, \ \-\-gallina
 Do not print proofs.
 
 .TP
-.B -l, \ --light
-Light mode. Suppress proofs (as with -g) and the following commands:
+.B \-l, \ \-\-light
+Light mode. Suppress proofs (as with \-g) and the following commands:
 
         * [Recursive] Tactic Definition
         * Hint / Hints
@@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands:
         * 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).
+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.
+.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/.
+.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
+.BI \-\-inputenc \ string
 Give a LATEX input encoding, as an option to LATEX package inputenc.
 
 .TP
-.BI --charset \ string
+.BI \-\-charset \ string
 Specify the HTML character set, to be inserted in the HTML header.
 
 
diff --git a/man/coqide.1 b/man/coqide.1
new file mode 100644
index 00000000..20379ef4
--- /dev/null
+++ b/man/coqide.1
@@ -0,0 +1,166 @@
+.TH COQIDE 1 "July 16, 2004"
+
+.SH NAME
+coqide \- The Coq Proof Assistant graphical interface
+
+
+.SH SYNOPSIS
+.B coqide
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is a gtk graphical interface for the Coq proof assistant.
+
+For command-line-oriented use of Coq, see
+.BR coqide (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
+.BI \-is\  f ,\ \-inputstate\  f
+Read state from
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\  f
+Write state in file
+.IR f .coq.
+.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\  f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\  f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.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 \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.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
+.BI \-user\  u
+Use the rcfile of user
+.IR u .
+.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.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+
+.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/coqmktop.1 b/man/coqmktop.1
index 3640d439..1b9c9e2a 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -17,10 +17,10 @@ coqmktop \- The Coq Proof Assistant user-tactics linker
 .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.
+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.
+directly or through coqc(1), using the \-image option.
 
 .SH OPTIONS
 
diff --git a/man/coqwc.1 b/man/coqwc.1
index 7011d148..4594aeec 100644
--- a/man/coqwc.1
+++ b/man/coqwc.1
@@ -44,4 +44,4 @@ Do not skip headers
 .SH BUGS
 
 Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr