summaryrefslogtreecommitdiff
path: root/man/coqmktop.1
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch)
treef672a286d962cc67c95874b3b60402fc957870b6 /man/coqmktop.1
parenta5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff)
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'man/coqmktop.1')
-rw-r--r--man/coqmktop.138
1 files changed, 38 insertions, 0 deletions
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),