1 files changed, 0 insertions, 166 deletions
diff --git a/debian/coqide.1 b/debian/coqide.1
deleted file mode 100644
index 20379ef4..00000000
--- a/debian/coqide.1
+++ /dev/null
@@ -1,166 +0,0 @@
-.TH COQIDE 1 "July 16, 2004"
-
-.SH NAME
-coqide \- The Coq Proof Assistant graphical interface
-
-
-.SH SYNOPSIS
-.B coqide
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B coqtop
-is a gtk graphical interface for the Coq proof assistant.
-
-For command-line-oriented use of Coq, see
-.BR coqide (1)
-; for batch-oriented use of Coq, see 
-.BR coqc (1).
-
-
-.SH OPTIONS
-
-.TP
-.B \-h
-Show the complete list of options accepted by
-.BR coqide .
-.TP
-.BI \-I\  dir ,\ \-include\  dir
-Add directory dir in the include path.
-.TP
-.BI \-R\  dir\ coqdir
-Recursively map physical
-.I dir
-to logical
-.IR coqdir .
-.TP
-.B \-src
-Add source directories in the include path.
-.TP
-.BI \-is\  f ,\ \-inputstate\  f
-Read state from
-.IR f .coq.
-.TP
-.B \-nois
-Start with an empty state.
-.TP
-.BI \-outputstate\  f
-Write state in file
-.IR f .coq.
-.TP
-.BI \-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 coqtop (1),
-.BR coq-tex (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual,
-.I
-The Coq web site: http://coq.inria.fr,
-.I
-/usr/share/doc/coqide/FAQ.
-
-.SH AUTHOR
-This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
-for the Debian project (but may be used by others).