diff options
Diffstat (limited to 'debian/coqc.1')
| -rw-r--r-- | debian/coqc.1 | 172 |
1 files changed, 0 insertions, 172 deletions
diff --git a/debian/coqc.1 b/debian/coqc.1 deleted file mode 100644 index baa04a88..00000000 --- a/debian/coqc.1 +++ /dev/null @@ -1,172 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coqc \- The Coq Proof Assistant compiler - - -.SH SYNOPSIS -.B coqc -[ -.B general \ Coq \ options -] -.I file - - -.SH DESCRIPTION - -.B coqc -is the batch compiler for the Coq Proof Assistant. -The options are basically the same as coqtop(1). -.IR file.v \& -is the vernacular file to compile. -.IR file \& -must be formed -only with the characters `a` to `Z`, `0`-`9` or `_` and must begin -with a letter. -The compiler produces an object file -.IR file.vo \&. - -For interactive use of Coq, see -.BR coqtop(1). - - -.SH OPTIONS - -.TP -.BI \-h -Show the whole list of options of coqc and coqtop. -.TP -.B \-verbose -Compile verbosely. -.TP -.BI \-image\ f -Specify an alternative executable for Coq. -.TP -.B \-t -Keep temporary files. -.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 coqtop (1), -.BR coq_makefile (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr |