diff options
Diffstat (limited to 'debian/coqmktop.1')
-rw-r--r-- | debian/coqmktop.1 | 70 |
1 files changed, 0 insertions, 70 deletions
diff --git a/debian/coqmktop.1 b/debian/coqmktop.1 deleted file mode 100644 index a35e436a..00000000 --- a/debian/coqmktop.1 +++ /dev/null @@ -1,70 +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 -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 |