diff options
Diffstat (limited to 'man')
| -rw-r--r-- | man/coqchk.1 | 8 | ||||
| -rw-r--r-- | man/coqmktop.1 | 71 |
2 files changed, 6 insertions, 73 deletions
diff --git a/man/coqchk.1 b/man/coqchk.1 index a00914eab8..f9241c0d47 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -34,13 +34,17 @@ add directory in the include path .TP -.BI \-R \ dir\ coqdir -recursively map physical +.BI \-Q \ dir\ coqdir +map physical .I dir to logical .I coqdir .TP +.BI \-R \ dir\ coqdir +synonymous for -Q + +.TP .BI \-silent makes coqchk less verbose. diff --git a/man/coqmktop.1 b/man/coqmktop.1 deleted file mode 100644 index 810df782c2..0000000000 --- a/man/coqmktop.1 +++ /dev/null @@ -1,71 +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 -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 -.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 |