Imported Upstream version 8.1~gammaupstream/8.1.gamma

4 files changed, 229 insertions, 17 deletions

diff --git a/man/coqc.1 b/man/coqc.1
index 741b3dcb..7113d504 100644
--- a/man/coqc.1
+++ b/man/coqc.1
@@ -32,10 +32,13 @@ For interactive use of Coq, see
 
 .SH OPTIONS
 
-.TP
-.BI \-h
-Will give you a description of the whole list of options of coqc and
-coqtop.
+.B coqc
+is a script that simply runs
+.B coqtop
+with option 
+.B \-compile
+it accepts the same options as
+.B coqtop.
 
 .SH SEE ALSO
 
diff --git a/man/coqdep.1 b/man/coqdep.1
index 01d080fc..6ae89f8b 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -23,6 +23,9 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
 [
 .BI \-D
 ]
+[
+.BI \-slash
+]
 .I filename ...
 .I directory ...
 
@@ -37,10 +40,11 @@ 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 and
+.IR Load \&
 commands. Dependencies relative to modules from the Coq library are not
 printed.
 
@@ -54,8 +58,7 @@ directives and the dot notation
 .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).
+(On Caml modules, the behaviour is exactly the same as ocamldep).
 .TP
 .BI \-w
 Prints a warning if a Coq command
@@ -78,6 +81,10 @@ 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 \-slash
+Prints paths using a slash instead of the OS specific separator. This
+option is useful when developping under Cygwin.
+.TP
 .BI \-I \ directory
 The files .v .ml .mli of the directory
 .IR directory \&
@@ -87,7 +94,7 @@ but their own dependencies are not printed.
 .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.
+be used under normal circumstances.
 
 
 .SH SEE ALSO
@@ -120,7 +127,7 @@ Consider the files (in the same directory):
 where
 .TP
 .BI \+ 
-D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ;
+D.ml contains the commands `open A', `open B' and `type t = C.t' ;
 .TP
 .BI \+
 Y.v contains the command `Require X' ;
@@ -135,7 +142,7 @@ example% coqdep -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.B Z.vo: Z.v ./X.vo ./D.cmo
 .B Y.vo: Y.v ./X.vo
 .B X.vo: X.v
 .fi
@@ -150,7 +157,7 @@ example% coqdep -w -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.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
@@ -167,10 +174,14 @@ 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
+.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
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index 05e73d75..3640d439 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -28,6 +28,44 @@ directly or through coqc(1), using the -image option.
 .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
+.B \-searchisos
+Build a toplevel for SearchIsos
+
+.TP
+.B \-ide
+Build a toplevel for the Coq IDE
+
+.TP
+.BI \-R \ dir
+Specify recursively directories for Ocaml
+
+.TP
+.B \-v8
+Link with V8 grammar
+
+
 .SH SEE ALSO
 
 .BR coqtop (1),
diff --git a/man/coqtop.1 b/man/coqtop.1
index d75b283f..a3b3aac4 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1 "October 11, 2006"
 
 .SH NAME
 coqtop \- The Coq Proof Assistant toplevel system
@@ -24,9 +24,169 @@ For batch-oriented use of Coq, see
 .SH OPTIONS
 
 .TP
-.B \-h
+.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
+.BI \-inputstate \ filename, \ \-is \ filename 
+read state from file
+.I filename.coq
+
+.TP
+.B \-nois
+start with an empty intial state
+
+.TP
+.BI \-outputstate filename
+write state in file
+.I filename.coq
+
+.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 \ filename
+load Coq object file
+.I filename.vo
+
+.TP
+.BI \-require \ filename
+load Coq object file
+.I filename.vo
+and import it (Require Import filename.)
+
+.TP
+.BI \-compile \ filename
+compile Coq file
+.I filename.v 
+(implies 
+.B \-batch
+)
+
+.TP
+.BI \-compile\-verbose \ filename
+verbosely compile Coq file
+.I filename.v
+(implies 
+.B \-batch
+)
+
+.TP
+.B \-opt
+run the native\-code version of Coq
+
+.TP
+.B \-byte
+run the bytecode version of Coq
+
+.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 \ filename
+set the rcfile to
+.I filename
+
+.TP
+.BI \-user \ uid
+use the rcfile of user
+.I uid
+
+
+.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
+.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
+
+.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 $COQ_XML_LIBRARY_ROOT (if set) or to
+stdout (if unset)
+
+.TP
+.B \-quality
+improve the legibility of the proof terms produced by
+some tactics
+
 .SH SEE ALSO
 
 .BR coqc (1),