1 files changed, 172 insertions, 0 deletions
diff --git a/debian/coqc.1 b/debian/coqc.1
new file mode 100644
index 00000000..baa04a88
--- /dev/null
+++ b/debian/coqc.1
@@ -0,0 +1,172 @@
+.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