Imported Upstream version 8.8.2upstream/8.8.2

6 files changed, 14 insertions, 97 deletions

diff --git a/man/coqchk.1 b/man/coqchk.1
index 76a7cfc5..f9241c0d 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -23,7 +23,7 @@ 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 name.
+short or qualified logical name, or by their filename.
 
 .SH OPTIONS
 
@@ -34,13 +34,17 @@ add directory
 in the include path
 
 .TP
-.BI \-R \ dir\ coqdir          
-recursively map physical
+.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.
 
diff --git a/man/coqdep.1 b/man/coqdep.1
index 81f7e1e0..c417402c 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -80,9 +80,12 @@ Prints the dependencies of Caml modules.
 \" 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 than for other
+Have the same effects on load path and modules names as for other
 coq commands (coqtop, coqc).
 .TP 
 .BI \-coqlib \ directory
diff --git a/man/coqide.1 b/man/coqide.1
index f82bf2ad..3592f6e4 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -123,13 +123,6 @@ 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
 
diff --git a/man/coqmktop.1 b/man/coqmktop.1
deleted file mode 100644
index 810df782..00000000
--- a/man/coqmktop.1
+++ /dev/null
@@ -1,71 +0,0 @@
-.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.
-
-.TP
-.BI \-srcdir \ dir
-Specify where the Coq source files are
-
-.TP
-.BI \-o \ exec\-file
-Specify the name of the resulting toplevel
-
-.TP
-.B \-opt
-Compile in native code
-
-.TP
-.B \-full
-Link high level tactics
-
-.TP
-.B \-top
-Build Coq on a ocaml toplevel (incompatible with
-.BR \-opt )
-
-.TP
-.BI \-R \ dir
-Specify recursively directories for Ocaml
-
-.TP
-.B \-v8
-Link with V8 grammar
-
-
-.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
index feee7fd8..084adfe4 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -110,7 +110,7 @@ print Coq version and exit
 
 .TP
 .B \-q
-skip loading of rcfile
+skip loading of rcfile (resource file) if any
 
 .TP
 .BI \-init\-file \ filename
@@ -140,12 +140,6 @@ dump globalizations in file f (to be used by
 )
 
 .TP
-.BI \-with\-geoproof \ (yes|no)
-to (de)activate special functions for Geoproof within Coqide (default is
-.I yes
-)
-
-.TP
 .B \-impredicative\-set
 set sort Set impredicative
 
@@ -153,12 +147,6 @@ set sort Set impredicative
 .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 $COQ_XML_LIBRARY_ROOT (if set) or to
-stdout (if unset)
-
 .SH SEE ALSO
 
 .BR coqc (1),
diff --git a/man/gallina.1 b/man/gallina.1
index 8c607216..f8879c45 100644
--- a/man/gallina.1
+++ b/man/gallina.1
@@ -29,7 +29,7 @@ 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
+reaches a command "Abort.", "Qed.", "Defined." or "Proof
 <...>.". It also removes every "Hint", "Syntax",
 "Immediate"  or "Transparent" command.
 
@@ -52,7 +52,7 @@ 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.
+"Qed." or "Abort." in a comment is not taken into account.
 
 
 .SH BUGS