Ajout de pages de man pour les exécutables coq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9233 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 207 insertions, 6 deletions

diff --git a/man/coqc.1 b/man/coqc.1
index 741b3dcb8..7113d5044 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/coqmktop.1 b/man/coqmktop.1
index 05e73d759..3640d439b 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 d75b283fd..a3b3aac40 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),