1 files changed, 70 insertions, 0 deletions
diff --git a/debian/coqmktop.1 b/debian/coqmktop.1
new file mode 100644
index 00000000..a35e436a
--- /dev/null
+++ b/debian/coqmktop.1
@@ -0,0 +1,70 @@
+.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
+Show a list of the available options.
+.TP
+.BI \-srcdir\  dir
+Specify where the Coq source files are.
+.TP
+.BI \-o\  exec\-fil
+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),
+.BR ocamlmktop (1).
+.BR ocamlc (1).
+.BR ocamlopt (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr