diff options
Diffstat (limited to 'debian/coqtop.1')
-rw-r--r-- | debian/coqtop.1 | 155 |
1 files changed, 0 insertions, 155 deletions
diff --git a/debian/coqtop.1 b/debian/coqtop.1 deleted file mode 100644 index b136a68b..00000000 --- a/debian/coqtop.1 +++ /dev/null @@ -1,155 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coqtop \- The Coq Proof Assistant toplevel system - - -.SH SYNOPSIS -.B coqtop -[ -.B options -] - -.SH DESCRIPTION - -.B coqtop -is the toplevel system of Coq, for interactive use. -It reads phrases on the standard input, and prints results on the -standard output. - -For batch-oriented use of Coq, see -.BR coqc (1). - - -.SH OPTIONS - -.TP -.B \-h -Show the complete list of options accepted by coqtop. -.TP -.BI \-I\ dir ,\ \-include\ dir -Add directory dir in the include path. -.TP -.BI \-R\ dir\ coqdir -Recursively map physical dir to logical coqdir. -.TP -.B \-src -Add source directories in the include path. -.TP -.BI \-is\ f ,\ \-inputstate\ f -Read state from file -.IR f .coq. -.TP -.B \-nois -Start with an empty state. -.TP -.BI \-outputstate\ f -Write state in file -.IR f .coq. -.TP -.BR \-load\-ml\-object\ f -Load ML object file -.IR f . -.TP -.BI \-load\-ml\-source\ f -Load ML file -.IR f . -.TP -.BI \-l\ f ,\ \-load\-vernac\-source\ f -Load Coq file -.IR f .v -(Load -.IR f .). -.TP -.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f -Load Coq file -.IR f .v -(Load Verbose -.IR f .). -.TP -.BI \-load\-vernac\-object\ f -Load Coq object file -.IR f .vo. -.TP -.BI \-require\ f -Load Coq object file -.IR f .vo -and import it (Require -.IR f .). -.TP -.BI \-compile\ f -Compile Coq file -.IR f .v -(implies -.BR \-batch ). -.TP -.BI \-compile\-verbose\ f -Verbosely compile Coq file -.IR f .v -(implies -.BR \-batch ). -.TP -.B \-opt -Run the native-code version of Coq or Coq_SearchIsos. -.TP -.B \-byte -Run the bytecode version of Coq or Coq_SearchIsos. -.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\ f -Set the rcfile to -.IR f . -.TP -.BI \-user\ u -Use the rcfile of user -.IR u . -.TP -.B \-batch -Batch mode (exits just after arguments parsing). -.TP -.B \-boot -Boot mode (implies -.B \-q -and -.BR \-batch ). -.TP -.B \-emacs -Tells Coq it is executed under Emacs. -.TP -.BI \-dump\-glob\ f -Dump globalizations in file -.I f -(to be used by -.BR coqdoc (1)). -.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 -.B COQ_XML_LIBRARY_ROOT -(if set) or to stdout (if unset). - - -.SH SEE ALSO - -.BR coqc (1), -.BR coq-tex (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr |